SELECTION_LEDGER.md

OPH Selection Ledger

Generated by tools/build_selection_ledger.py from claims/selection_ledger.json; edit the JSON, then regenerate.

OPH builds public reality from finite observers that read patches of a shared screen, compare overlaps, and repair disagreement until every observer agrees. On the declared carrier lineage (row 4, an exposed premise) that consensus requirement forces the pairing and frame of rows 2-3. The unit split in row 1 is exact inside a separately declared integer counting and cost realization. These statements have machine-checked proofs. Finite menus are enumerated where they exist. Other exposed premises include continuous data or unenumerated maps and are excluded from finite compression accounting. Across the premise register and this ledger, declared inputs and unresolved attachments are named. This ledger is the bounded discrete-selection and compression inventory defined in claims/selection_ledger.json; it is not an exhaustive inventory of every theorem premise. Declared effects, evolution laws, scheduler clauses, and finite action packets belong in the premise register. Rows here are classified as FORCED (derived from the axioms and source objects), EXPOSED PREMISE (chosen and declared in theorem antecedents), or OPEN (neither, with the owning GitHub issue). It shows what is proved and open inside this finite menu: pick an open row and work on it. It is the free-versus-forced surface for historical issue #554; the premise register was established under #727 and remains a maintained scientific register, and source discharge is #739.

Forced by consensus

#	Selection	Where it is forced	Menu beaten
2	Inverse port pairing and six axes	Issue #565 closure packet: unique distance-3 antipodal pairing and six axes on the port incidence, with negative controls. Conditional on row 4.	10395 (fixed-point-free pairings of twelve labels; 10,395 pairings exist without incidence and oriented incidence at distance three selects the antipodal pairing uniquely)
3	Icosahedral oriented action (A5 versus orientation-forgetting A5 x C2)	Issue #565 closure packet: Aut+ isomorphic to A5 and full Aut isomorphic to A5 x C2. Lean: Lean/Screen/A5PortAction.lean (kernel decide). Conditional on row 4. OPH-SCREEN-GALOIS-FRAME-BOUNDARY separately certifies an additional unselected ambiguity within a frozen Gram pair. The marked-triplet attachment certificate separately distinguishes the native spatial and internal representation domains under the same action; incidence recharting does not supply their representation attachment or a physical golden-embedding selector.	2 (oriented A5 frame or orientation-forgetting A5 x C2 frame; the orientation receipt fixes the oriented class)
11	A1/A2 compact port-current Lie type	A1 supplies a faithful complete compact twelve-dimensional port response and A2 makes every proper carrier recharting internal to that response. The carrier has one fixed line. Compact classification and the centreless four-factor fixed-space exclusion leave only u(1)+su(2)+su(3). Target-blind readback separately derives R=-J. The charged-double-triplet matrices are an exact declared witness. A bounded inventory of 33 source/runtime/formal/physical-current packets, including routed histories, native temporal and publication constructions, finite-state controls, registered all-port reads and supplied flagged recovery, finds zero object carrying all required ordered raw W12 perturbation data and refinement provenance within the enumerated reviewed source scope. The inventory does not exclude another producer. No ordered source tomography or same-current holonomy follows. Conditional on row 4.	2 (the centreless su(2)^4 branch or the one-centre u(1)+su(2)+su(3) branch after the A1/A2 centre bound)

Exposed premises

#	Selection	Where it is declared	Menu
1	Twelve-unit port splitting (all twelve port weights equal one)	Within the declared integer record-counting grammar q in Z^12 with sum q=12 and the declared normalized central-readback cost H(q)=sum q_i^2, the executable #565 packet proves that the all-one vector is the unique minimizer over the full integer lattice, with floor 12, next floor 14, and gap 2. Lean/Screen/UnitSplit12.lean proves the positive-natural sum-12 special case. The complete #625 diagram theorem fixes additive record counting up to one positive unit scale. The #628 operational patch mechanism generates integer counts from atomic signed events and derives a move-count settling cost from conservative register repairs. Its exact Lyapunov function is the load square, not the seam quadratic or the A3 Hessian; the readback scale remains a unit convention. Conditional on row 4 and these named-realization premises.	1352078 (weak nonnegative integer compositions of 12 into twelve slots; all 1,352,078 compositions minimize the linear cost sum q_i=12, while the declared quadratic cost selects the all-unit composition uniquely)
4	A1 icosahedral boundary packet and declared Echosahedral lineage	A1 declares that each finite local carrier has twelve primitive ports with the unlabeled 12-vertex, 30-edge, 20-face, degree-five, coherently oriented boundary complex of the icosahedron. This local boundary architecture is axiom content. The richer Echosahedral lineage, including its counting realization, response law, and physical carrier identification, is separately declared or source-gated and does not follow from the boundary combinatorics alone. Lean Lean/Screen/PhysicalA5ForcingNoGo.lean (noSourceOnlyChargeReconstruction) proves that the bare total-charge reduct cannot reconstruct even the boundary choice. Conditional on a supplied SL(2, F_5) source, code/a5_closure/coset_carrier_certificate.py reconstructs this boundary complex as the coset geometry of the central quotient and relabels it onto the committed port frame, so the packet is derived rather than separately supplied once that group is given; the certificate does not select the source group (discussion 769).	3 (tetrahedral, octahedral, icosahedral antipodal port families)
5	Compact-gauge refinement receipt	Declared in the D7 antecedent of The Standard Model gauge paper and the synthesis paper: cofinal tail with coherent surjective charge pullbacks, finite block embeddings, tensor realizations, 3+1D symmetry, and compatible forgetful fibers.	declared receipt object; no finite alternative enumeration exists, so the row is a theorem antecedent and not a compression-menu input
6	Declared matter completion with the one-generation/one-Higgs witness	The completed matter packet carries separately declared three-generation and one-Higgs completions inside the conditional window 3 <= N_g <= 5 given by the CP-capability and weak-sector clauses. The one-generation chiral witness is realized exactly; the generation count, scalar multiplicity, and extra-sector completeness are open physical attachments, and no minimality argument enters any conclusion. The executed campaigns bound them exactly: the window edges are exact, the in-window count and scalar count are not source-determined, and extra light sectors are excludable only inside the declared algebra (receipts multiplicity_window_reference and matter_menu_spectral_ledger_reference).	3 (the conditional window admits N_g in {3, 4, 5}; the declared completion displays three without selecting it)
7	BR-0: cell product reading of the screen count	code/capacity_readback/F_CONSTRUCTION_2026-07-14.md, Step 2: reading (i) is the only executable reading and is carried with its warning as an inherited hypothesis; it reproduces the declared screen dimension exactly.	2 (reading (i) treats the cells as independent record carriers; reading (ii) refuses the product structure and derives no count)
8	Publicness policy	Frozen publicness policy declared in the finite closure construction of the synthesis paper; deriving it from source objects belongs to the H1 issue #736 program.	frozen policy object; no finite alternative enumeration exists, so the row is a theorem antecedent and not a compression-menu input
9	Scheduler selection (fair-block contraction branch)	Declared in the consensus-paper fair-block antecedent, where the implementation supplies the contraction data for the statement.	declared branch with continuous contraction data; no finite alternative enumeration exists, so the row is a theorem antecedent and not a compression-menu input
12	Declared-lattice Z6 descent and open physical global form	The descent certificate computes the common Z6 kernel on every declared matter tensor by exhaustive enumeration over 36 candidates and derives the central descent congruence with Smith invariants (1, 1, 6). Local tensors descend through the cover and the Z2, Z3, and Z6 quotients and cannot select a physical form. The six-axis class has order six only after its diagonal and zero-sum coefficient relations are declared. The exact intertwiner and electric-polarization result hold inside that declared system. Source selection of the relation lattice, complete source characters, the same-source loop-to-kernel identity, and laboratory attachment are open. Conditional on rows 4, 12, and 14.	4 (the four locally admissible forms: cover, Z2, Z3, and Z6 quotients; the declared order-six coefficient system matches the Z6 menu without selecting it physically)
13	Conditional exterior matter and finite Spin fixture	Inside the declared charged-double-triplet and exterior CAR/Fock construction, the exhaustive 1024-subset anomaly scan leaves the unordered conjugate rank-15 pair as the unique nonempty chiral anomaly-free selection and outputs its fermionic-parity grading. The finite non-split transport double cover fixes the Spin/odd-Weyl typing inside that fixture. The upstream current representation, physical matter action, one conjugate representative, continuum Spin attachment, scalar existence, and extra-light-sector completeness are not source-selected. Conditional on rows 4 and 12.	1024 (all 1024 subsets of the ten nontrivial isotypic components; exactly two survive chirality and the four anomaly constraints, and they form one unordered conjugate pair equal to the two fermionic-parity sectors)
23	B13 post-hoc repair-count statistic and completion pairing	RepairCurrentOrientation.lean mirrors a post-hoc raw-count product-gap statistic whose statistic, maximizing cycle, and tie-break rule were not preregistered. SourceOrientedCompletion.lean then declares one of the two possible pairings between its Bool value and the conjugate phase-completion pair; the opposite pairing is equally admissible. The applicability proof is threaded through the API, but neither the statistic nor pairing is source-selected or eligible as validation.	the two explicit torsor pairings sit inside an unenumerated space of possible post-hoc statistics and designation rules; no source-derived menu was frozen
24	Finite native observer tape, detector and continuation design	model/observer/ specifies a two-event tape, uniform binary preparation, supplied forecast, record-only seam controller and halt. Its capacity adapter declares exact terminal reread and reached-prefix encoding. model/observer/p_response/ additionally specifies charge Q_v=g(P)N_v, a prepared path qubit, calibrated external exposure and a bit-only actuator while consuming the declared P coupling map. model/local_tick/ separately supplies the N4 tracial preparation, uniform schedule, incident detector and bare occupation reads. These are implemented finite designs with completed scoped checks. Their validity does not require proving that self-consistency uniquely selects the design. Physical field, clock, hardware and whole-universe attachments keep their separate premises. model/observer/scalar_response/ supplies the scalar Hamiltonian and original vacuum, signed native-current preparation, binary Weyl branch instrument, fixed model-time window and bit-only native continuation. Its inherited golden refinement compares this same designed detector; the Hamiltonian is not selected by integer averaging. model/SOURCE_SELECTION.md organizes the target into carrier architecture, observer interface and implementation, and complete repair rule. The coherent native continuation and source-executed record-phase tests leave these obligations conditional: structural covariance does not select the continuation, committed histories hide scalar branch phases, and a declared pre-commitment X read exposes 3/4 versus 1/4 for source implementations of the same committed C/E instrument. The record algebra, coherent access and readout remain interface choices; the complementary label is not a simultaneous native current. These tests add no forced selection or new compression menu.	No finite enumeration of apparatus, memory, exposure or continuation designs is claimed.

Open: the work-wanted list

#	Selection	Owner and state	Menu state
10	Quantitative closure map declaration (pixel closure)	Two declared mathematical closure maps have disjoint interval-certified contraction fixed points on their analytic domains (Standard Model gauge derivation, certificate C1). Neither map is source-selected, and no pinned parent constructs detuning and return as readings of one invariant. Same-scheme Thomson transport is a separate receipt. A third code-side output, the compressed P-closure trunk (code/P_derivation/runtime/p_closure_trunk_current.json: P = 1.6309721049, inverse coupling 136.9940207), adds a structured low-energy running layer without the hadronic payload. This is an approximate candidate, not an interval-certified fixed point; its printed-pair identity has relative defect about 5.2452e-6. It may not feed predictions. The frozen source-only preflight pins its bytes as evidence that the P side is not promotable; promotion or retirement remains owned by #736. The retained history therefore contains two certified roots (inverse couplings 136.994835 and 137.035660) and one approximate output (136.9940207). Separately, the retrospective constant-substitution scorecard contains 48 labels representing 42 distinct numerical pairs, including the declared pair and 41 alternatives. The selection-accounting receipt independently reconciles these counts, the seven electron-exponent candidates 5 through 11, and the certification boundary. Neither this retained history nor the substitution grid is an exhaustive, precomparison map-form menu. Counts and numerical coverage do not identify a chance probability without a sampling measure and selection rule, as the receipt demonstrates with two probability measures on the same outputs. Owner: #736.	per declared map; the map space has no finite alternative enumeration, so the row is a theorem antecedent and not a compression-menu input
14	Rank-three screen response and conditional family candidate	The exact band-cost order uniquely selects the rank-three screen band under the single-complete-band realization and operational cost premises. The declared unitary simulator recovers its residue at the lowest positive generator frequency and conserves mode norms. Tensoring the band with the declared fifteen-state generation table gives a conditional complex rank-45 candidate. Chirality and the diagonal Z6 action are arithmetic properties of that table. A separate finite local-domain receipt checks the declared operator D_sigma tensor I_45 and conditional inheritance of the signed seam operator's positive gap. The source does not select that matter action. The twelve-port Spin packet and the 8662-node local domain have no certified source, domain, or transport bridge. Physical matter-pole identification, continuum Spin/locality, physical seam selection, the third persistence leg, and laboratory-current attachment are undischarged under issue #736. The exact 31-axis spectrum excludes only direct real-3D residual-axis equality with the Cabibbo angle. Owner: #736.	the attachment menu is not enumerated; spinorial, broken-symmetry, and general overlap routes are open
15	Capacity-closure selector (required one-zero law open)	The exact generation-register counterfamily has incompatible slack-zero sets under its bounded premises, and transported source controls pass on six finite rungs. The source-only audit derives thirty entries, including the declared seventeen-row menu for the executed capacity families and five hierarchy packets. Fifteen entries have exact fixed-point progress, while none qualifies under all seven row gates. Four of five preflight-completion gates remain open. This is a bounded inventory result rather than exhaustive future-law nonidentifiability. Universal all-rung membership in the complete A1-A3 source class and the executable-to-Lean bridge are unproved. The closed #708 preflight's premise list assigns the source-only selector, same-quantity construction, return map, and completion continuation to #736. Issue #729 owns the common source-derived tower and Einstein-branch attachments. Issue #736 owns final physical integration. Owner: #736, #729.	the closure-selector menu is not enumerated before the slack law exists
16	BR-1: reserve semantics	Declared menu in F_CONSTRUCTION_2026-07-14.md, Step 3. The #649 packet proves that the normalized finite-cut datum and declared composition laws do not select a global action. It does not resolve this menu. The closed #708 preflight's premise list assigns target-independent source selection to #736; issue #736 owns the later physical integration. Owner: #736.	3 (poisson survival e^(-P/24), presence survival 1 - P/24, or no exclusion)
17	BR-2: reserve attachment	Declared menu in F_CONSTRUCTION_2026-07-14.md, Step 3. The #649 packet proves that the normalized finite-cut datum and declared composition laws do not select a global action. It does not resolve this menu. The closed #708 preflight's premise list assigns target-independent source selection to #736; issue #736 owns the later physical integration. Owner: #736.	2 (one reserve unit per equal-area cell, or reserve priced on the 3K shared edges)
18	BR-3: count effect of the readback record	Declared menu in F_CONSTRUCTION_2026-07-14.md, Step 4. The #649 packet proves that the normalized finite-cut datum and declared composition laws do not select a global action. It does not resolve this menu. The closed #708 preflight's premise list assigns target-independent source selection to #736; issue #736 owns the later physical integration. Owner: #736.	4 (port multiplicity X+, delta constraint X0, record cost X-, write plus check cost X=)
19	BR-4: observer/checkpoint subfederation marking	Declared menu in F_CONSTRUCTION_2026-07-14.md, Step 5. The #649 packet proves that the normalized finite-cut datum and declared composition laws do not select a global action. It does not resolve this menu. The closed #708 preflight's premise list assigns target-independent source selection to #736; issue #736 owns the later physical integration. Owner: #736.	3 (unmarked K0, one marked chain K1, chain plus checkpoint K2)
20	BR-5: symmetry quotient	Declared menu in F_CONSTRUCTION_2026-07-14.md, Step 6. The #649 packet proves that the normalized finite-cut datum and declared composition laws do not select a global action. It does not resolve this menu. The closed #708 preflight's premise list assigns target-independent source selection to #736; issue #736 owns the later physical integration. Owner: #736.	3 (A5 quotient S-, quotient representatives S0, flag multiplicity S+)
21	BR-6: Cap_read family	Declared menu in F_CONSTRUCTION_2026-07-14.md, Step 7. The #649 packet proves that the normalized finite-cut datum and declared composition laws do not select a global action. It does not resolve this menu. The closed #708 preflight's premise list assigns target-independent source selection to #736; issue #736 owns the later physical integration. Owner: #736.	4 (CAP-L log-count readback and three declared alternative Cap_read families; CAP-B is barred before evaluation)
22	B14 oriented-face Jacobi repair rule	The declared equal-weight cyclic rule on the twenty pinned oriented faces gives exactly 60 R13 and an exact 240-coordinate Jacobi failure. On the same 792 upper-triangular coordinates, exact primal-dual certificates make family G win total absolute, squared Euclidean, and worst-coordinate edit comparisons with the classified compact locus; the competing F total-edit value is an unattained infimum. Neither the equal-weight rule, any of the three basis-dependent norms, nor minimum-distance Jacobi repair is derived from the OPH source, so physical bracket selection is undischarged. Owner: #734.	no source-derived finite menu of Jacobi-repair laws has been enumerated

Totals: 24 selections. 3 FORCED, 11 EXPOSED PREMISE, 10 OPEN. Open rows belong to bracket, particle-realization, and capacity programs; the recovery of relativity and quantum structure from observer consensus consumes only the forced rows and declared premises above.

How to read a row

A FORCED row is a theorem: given the axioms and the cited premises, the selection has no alternative, the citation names the machine-checked or certified proof, and the menu column records the enumerated alternative set the theorem excluded. An EXPOSED PREMISE row is a declared choice: the theorem downstream of it states the choice in its antecedent, and the menu column records how many alternatives the declaration passed over. An OPEN row is a selection that is neither derived nor stated as a clean antecedent; the owning issue tracks the work that moves it into one of the other two classes. A row can move up (OPEN to EXPOSED PREMISE to FORCED) and never silently disappears: the consensus argument is exactly as strong as the FORCED column plus the declared premises it names. Rows with a numeric menu feed the compression accounting in claims/physical_identification_registry.json; rows whose declared object has no finite alternative enumeration carry their antecedent location instead and are excluded from compression accounting by construction. Every open row is a well-posed problem with an issue link; solving one moves it up the ledger.