# Selected additions to the single Boone–Higman Palomar package

Decision: 20 September 2026. The user explicitly selected the strongest results
and open-problem answers from all three supplied manuscripts for the combined
Palomar submission, and instructed us to use the manuscripts as correct working
proofs, repairing details as needed. These results are **included in the intended
scope**, not optional candidates awaiting another approval or an independent
referee's permission. The earlier linear, metabelian, self-similar, graph-product,
ascending-HNN and four construction/permutation endpoints remain in scope.

This is a statement inventory and implementation contract. Inclusion here does
not assert that a corresponding closed Lean theorem already exists. Cairn proof
obligations remain visible until discharged. No manuscript result may enter the
verified Comparator theorem list as an axiom, a `sorry`, or a theorem conditional
on its own unproved host or finiteness theorem. The current four-name Comparator
configuration is a development checkpoint, not the selected final package.

## Headline additions

| Included result | Exact strength to retain | Source and formalization obligations |
| --- | --- | --- |
| Bilaterally observed mapping tori and twisted V lamps | For every finite `k≥2` and for `F_∞`, a type-`F_k` group `D`, automorphism `φ`, and homomorphism `ρ:D→V` with both one-sided intersections of iterate kernels trivial: `V^(ℤ)⋊T(D,φ)` embeds in a simple type-`F_k` group generated by two finite-order elements. The mapping torus and every automorphism of a type-`F_k` subgroup of `V` are explicit corollaries. Preserve the convention `t⁻¹gt=φ(g)` and the noninjective-observation generality. | [Mapping-torus proof](../research/artifacts/beyond-polynomial-germs/mapping-tori-and-compact-core.md). Formalize the compact-core SingFix theorem, distinct forward/backward endpoint species, exact bridge, finite-forest restriction groups, and BHM/BZ inputs. |
| Recurrent twists of nilpotent lamps | For all `m,q≥2`, finitely many integer bilateral profiles with independently eventual recurrent tails, the constant profile, and their translate module `𝓕`: `UT_m(ℤ[1/q])^(ℤ)⋊(𝓕⋊ℤ)` embeds in a two-finite-order-generator simple `F_∞` group. Permit different end recurrences and arbitrary finite exceptions. | [Recurrence proof §§1–6](../research/artifacts/beyond-polynomial-germs/recurrence-and-matrix-proofs.md). Formalize the finite forward integral lattice, arithmetic coset-tree base, full depth-zero isotropy, compact-core finiteness and shellwise faithfulness. |
| Noncommuting matrix twists | Vector lamps `ℤ[1/q]^r` with the profile group generated by translates of finitely many `q^(a_i(n))U_i(n)`, all constant `UT_r(ℤ)` matrices and `qI`, where every exponent/entry has recurrent tails, admit the same simple `F_∞` host. Do not replace this by commuting scalar twists. | [Matrix proof §§8–9](../research/artifacts/beyond-polynomial-germs/recurrence-and-matrix-proofs.md). Prove bounded-weight coefficient closure, finite generation of the entire nilpotent profile group, inclusion of full base isotropy and the faithful affine shell action. |
| Exact scalar-germ classification | For finitely many eventually integral one-sided profiles, with `M` generated by their germs, `1`, and all positive/negative shifts: eventual recurrence ⇔ finite rational rank of `M` ⇔ finite presentation of `M⋊ℤ` ⇔ type `F_∞`. | [Criterion §§1–4](../research/artifacts/beyond-polynomial-germs/recurrence-and-matrix-proofs.md). Prove both the forward-lattice construction and finite-window HNN stabilization/Britton converse. This is not an assertion that nonrecurrent lamp groups fail BH. |
| Decidable perfect envelope with an ineffective unique simple quotient | One finitely presented perfect group `E` with decidable word problem, a co-c.e. non-c.e. unique maximal proper normal subgroup `M`, infinite simple non-recursively-presentable `E/M`, an infinite finitely presented simple core whose every nonidentity element normally generates `E`, and a type-[A₂] action with kernel `M`. Preserve the impossibility of an exact normal-pair embedding into any finitely presented target with finitely normally generated distinguished kernel. | [Direct padded RN proof](../research/artifacts/padded-abstract-rn-manuscript-integration-2026-09-20.md). Formalize the finite-recursion input and repair, abstract table presentation, padding/commutator construction, formal support and clopen stabilizers. This obstructs a quotient strategy and does not disprove BH. |
| A concrete nonlinear solvable family | For every `q,a≥2`, the group generated by the unit lamp `A`, shift `X`, and twist `q^(a^abs(n))` is torsion-free, has derived length exactly three, is nonlinear over every field, and embeds in a two-finite-order-generator simple `F_∞` group. State “generated by three elements,” without claiming the minimum generator number unless separately proved. | [Concrete family §7](../research/artifacts/beyond-polynomial-germs/recurrence-and-matrix-proofs.md). Retain the nonzero second-derived witness, all-field eigenvalue/logarithm obstruction and recurrence-host application. |
| Recurrence Röver–Nekrashevych finiteness | The explicit self-similar groups formed from the arithmetic affine bases and the finite recurrence radial profile groups have RN groups of type `F_∞` in every finite forest, without assuming the enlarged state group itself is `F_∞`. Include the stated noncontracting examples. | [RN identification §10](../research/artifacts/beyond-polynomial-germs/recurrence-and-matrix-proofs.md). Prove self-similarity and equality with the full finite-germ extension, rather than only an inclusion. |
| Unary polynomial-function obstruction | A finitely presented group with decidable word problem whose group of unary polynomial functions is not recursively presentable. | [Audit integration: subsidiary proofs](../research/artifacts/boone-higman-cairn-integration-2026-09-20.md). Formalize the direct wreath presentation and exact kernel reduction, using the direct RN witness rather than an unproved kernel-removal shortcut. |

## Open-question answers and visible corollaries

These must appear in the combined narrative and theorem inventory with exact
quantifiers. They are grouped under their mechanisms rather than advertised as
independent discoveries.

| Included consequence | Treatment |
| --- | --- |
| FFWZ Question 5.8: yes | Derive from the faithful image of the type-[A₂] action. Reconcile the existing formal Q5.8 witness with the stronger direct witness and state which theorem certifies which construction. |
| FFWZ Question 5.9, both parts: no | Preserve exact pair intersection `j(E)∩L=j(M)` and both target specifications. The stronger no-embedding statement above implies these negative answers. Cairn already claimed the answers; the direct unified witness is the refinement. |
| Cairn's open q-difference lamplighter target | Include an explicit specialization `m=2`, linear exponent profile, recovering the Heisenberg top action and a simple `F_∞` host. Identify this as an archive-open target, not an independently established public-priority claim. |
| Polynomial, eventual-polynomial and fixed-period quasipolynomial twists | Expose specializations of the recurrence host wherever the complete global profile module is finitely generated under translation. Preserve the whole-group versions and finite exceptions, not just selected finitely generated subgroups. |
| Independent arithmetic dilations | Include the supplied multi-prime polynomial family over `ℤ[S⁻¹]` with its free-abelian germ quotients. This needs the multiscaling actor proof; it is not silently absorbed by a one-scalar recurrence theorem. |
| Finite products and finite extensions | Include the supplied actor permanence results with a finite quotient in the wreath embedding. Do not replace an unrestricted wreath product by a restricted one for an infinite quotient. |
| Noninjective Jordan/free-product observations | Include `D=ℤ^r*F_s` with the unipotent observation formula and the mapping-torus amalgam. For `r≥2` the inability of `D` to embed in `V` explains why bilateral observation is stronger than the subgroup-of-`V` corollary. Individual amalgam priority is not asserted. |
| Exact kernel-removal criterion and effective perfect envelope | Retain as supporting certified results in the direct obstruction development; avoid counting the corrected inverse-diagonal error as a new BH solution. |

## Proof order and release boundary

1. Continue the shared linear/metabelian/H1 and PBH development already underway.
2. Build common formal vocabulary for type `F_k`/`F_∞`, finite germ extensions,
   oligomorphic actions and finite-subset stabilizers; prove the actual BHM,
   SZ and BZ inputs needed by the selected theorems.
3. Formalize compact-core stabilizers and finite-forest restrictions once, then
   instantiate the mapping-torus and arithmetic recurrence/matrix families.
4. Prove the algebraic scalar criterion and concrete-family properties; derive
   polynomial and q-difference corollaries from the stronger recurrence route.
5. Close the direct RN witness and its question/polynomial-function consequences.
6. Extend the one challenge/solution pair, Comparator list, metadata,
   statement-report drivers, axiom audit and CI together as closed declarations
   become available. Remove superseded standalone BH submission surfaces after
   their consumers are migrated. Run the final Comparator and independent
   kernel replay on the complete immutable package before submission.

The user's working-proof instruction removes an independent-review waiting
condition from implementation. It does not turn a finite formula replay into
a Lean proof, permit additional axioms, or establish publication priority.
The selected scope does not include claiming a solution of full BH, FFWZ 5.7,
arbitrary linear-group mapping tori, arbitrary injective-endomorphism versions
of the observation theorem, or the general contracting-RN finiteness conjecture.
The separately intended free-group ascending-HNN result retains its own proof.