Exact finite contracts, controls, and archived candidate audits for the OPH capacity map. The canonical Pro5 producer is
N = log M_0(U_N),
F_set,r,epsilon(D) = {M_epsilon(q): q in Omega_tilde(r,D)},
M_0(q) = alpha(G_q).
The first line is the direct global proposal; the next two lines are its typed finite implementation.
The operational resolution, electroweak/Higgs bridge, and measured
cosmological constant are independent downstream comparisons. They never
define the direct map. The bounded counterfamily has verdict
NOT_EVALUABLE_INCOMPLETE_CAPACITY_SOURCE_ANTECEDENT. The
generation-register packet supplies exact all-rung capacity arithmetic and
finite source-contract checks on rungs one through six. Universal all-rung
membership in the complete A1--A3 source contract and the executable-to-Lean
membership bridge are open. No universe-level physical N is emitted.
The independent finite (A_5) control is summarized in
A5_FINITE_CONTROL_STATUS_2026-07-20.md.
It proves (M_0=60) on a complete bounded software packet and
(D_{\rm raw}=60k), but its publicly inert multiplicity makes raw dimension
implementation-dependent. It is a no-go control for physical promotion, not a
second physical packet or a cosmic selector.
CHECKPOINT_CHANNEL_AUDIT.mdrecords the exact channel contract, decoder-search correctness argument, independent replay and exhaustive controls, and downstream receipt comparison for the public-checkpoint numerical repair under issue #1033.F_READBACK_SPEC.mdis the Pro5 acceptance contract: complete terminal fiber, atom readouts, endogenous reachability, frozen publicness, global joint kernels, compound confusability graph, exact and approximate correctable capacity, carrier saturation, scalarization, refinement, finite-size slack, receipts, and controls.correctable_public_record_capacity.pyevaluates finite public checkpoint packets. It computes global sections, exact maximum independent sets, receipt-scale worst-input approximate capacities, support semigroups, carrier bounds, terminal-fiber scalarization, no-new-confusability, greatest fixed points, and unique slack-zero certificates.public_record_csp.pyis the exact constraint-propagating global-section backend. It is extensionally equivalent to Cartesian enumeration, but it model-counts the connected twelve-observer, twenty-four-atom source packet without exploring24^12assignments.PUBLIC_RECORD_GLUING_AUDIT.mdrecords the exact finite gluing repair, injective record identifiers, independent completeness replay, and unchanged downstream source receipts under #1033.test_correctable_public_record_capacity.pycovers saturation, cyclic permutation, joint-coupling nonidentifiability, approximate capacity, ambiguous fibers, order countermodels, target taint, and carrier failures.reversible_public_checkpoint_packet.pyretains the finite twelve-port icosahedral reference control. It verifies every checkpoint generator is a permutation, certifiesM_0(q)=|X_reach(q)|, and emits exact rank-one saturation. It remains explicitly nonphysical.test_reversible_public_checkpoint_packet.pychecks the 12 vertices, 30 interfaces, exact reversible capacity identity, noninjective failure, and target-taint failure.source_derived_public_checkpoint_packet.pydefines the first source-derived fixed-cutoff physical packet for issue #548. It freezes the carrier to the twelve edge-center ports with reversible write/check orientation, soD=|P_12 x {write,check}|=24. The producer emits:- a complete 67-world structural one-fault trial manifest with one terminal world, fully materialized candidates, SHA-256 completeness receipts, and an output-blind membership predicate;
- total observer/interface atom readouts and 24 endogenous reachability histories;
- a frozen universal publicness policy;
- the complete 40-element
D5 x C2 x C2joint checkpoint family, all 1,600 support-relation compositions, and independently checked local marginals; - an empty compound graph, a 24-record independent set, inverse decoders, worst-input and total-variation receipts;
- 24 orthogonal rank-one carrier projections, proving
M_epsilon <= 24and exact saturationM_0=24; - empty/incomplete/ambiguous/singleton fiber controls; isomorphism, cyclic, alternative-coupling, tiny-noise, circular-definition, taint, identity, erasure, and finite-suffix controls; and separate extension/refinement no-new-confusability injections with negative controls.
test_source_derived_public_checkpoint_packet.pychecks the full issue #548 acceptance surface.test_source_checkpoint_source_binding.pychecks the supplied operations against an independent port-coordinate oracle. The source certificate binds every named continuation to its action on the actual public sections, replays every declared composition on those sections, and compares complete local marginals exactly. Capacity, invertibility and an abstract group table alone do not establish that binding: reversing the named rotations preserves all three while changing the source operation. Reordered maps and explicit zero probabilities remain valid.test_source_checkpoint_evidence.py,test_source_checkpoint_provenance.pyandtest_source_checkpoint_generators.pychallenge the actual diagram, carrier projections, complete terminal-trial census, endogenous event histories and declared generating set. Rehashed false evidence is refused through the public certificate and its serialized direct-N consumer. Equivalent presentations and alternative valid executions remain admissible; a content hash alone is not a source proof.ISSUE_548_SOLUTION.mdmaps every acceptance item to the executable receipt.capacity_indexed_source_family.pygenerates four target-clean continuation completions at every positive rung. Reversible identity, copy collapse, a two-class cap, and hidden spectator multiplicity have different exact slack-zero sets while sharing the declared bounded antecedent.ISSUE_551_RESULT.mdstates the bounded counterfamily theorem and its boundary. The all-rung fixed-set disagreement is also proved inLean/ObserverPatchHolography/CapacityNonidentifiability.lean.direct_n_closure_verdict.pyconsumes that result in the direct global proposal and records that no numeric cosmic value or cosmological comparison is permitted.public_record_capacity.pyand its tests retain the superseded Pro4 checkpoint-fixed projection branch as a control. A cyclic permutation proves that it is not the canonical capacity definition.
The D=24 artifact is a source-derived fixed-cutoff packet in the declared
simulator category. The all-rung counterfamily proves nonidentifiability for
the base-agreement, positivity, and carrier-bound completion class. The
generation-register audit transports terminal-fiber, A2, A3, sewing,
extension, and refinement controls across six finite rungs. Its exact
capacity formulas extend to every positive rung, while membership of the
executable family in the complete source contract has no all-rung theorem.
The bounded receipt lives in
complete_packet_capacity_lift.py with
the no-producer-import replay in
verify_complete_packet_lift_independent.py,
the consuming issue #505 verdict is
NOT_EVALUABLE_INCOMPLETE_CAPACITY_SOURCE_ANTECEDENT, and the issue
#589 horizon exit NOT_EVALUABLE_NO_HORIZON_RECORD_ATTACHMENT is recorded by
horizon_record_attachment_verdict.py.
The screen value 24 is not a cosmic result.
python3 source_derived_public_checkpoint_packet.py --output-dir runtimeThis writes the complete terminal-fiber manifest, public checkpoint packet, and certificate as canonical JSON.
operational_readback_contract.pyevaluates frozen scale-discrimination errors, preserves pre/post-checkpoint accounting, requires complete-fiber agreement forrho_op, and compareslog M_0withpi/rho_op^2only after direct capacity exists.test_operational_readback_contract.pychecks discrimination endpoints, all-coarser thresholding, capped error accounting, complete-fiber agreement, and independence controls.
The diagnostic residual is
R_rho = log M_0 - pi/rho_op^2.
Defining rho_op from M_0, or using capacity to select its protocol,
invalidates the comparison.
These bridges consume a unique-zero direct closure. The bounded generation-register packet does not supply one, so they remain contracts with no evaluable capacity-side carrier:
- identifying the correctable record carrier with the de Sitter horizon may
identify
log D_starwithA/(4 ell_star^2)and yieldLambda ell_star^2=3*pi/N_star; - a positive refinement-natural carrier map may identify the source-normalized screen load with
the four-copy weak load and test
N_bridge=pi*exp(6*pi/(P*alpha_U(P))).
Neither bridge constructs the direct map. The exterior package proves the weak multiplicity four, but that integer alone does not identify a physical load carrier.
The dated construction notes and F_candidate_*.py files preserve historical
count, affine, and Banach candidates. They have diagnostic value only. The
CP* and G2_GAP_1 notes likewise do not supply the exact finite-size
selector.
- prove every transported source-contract control for every positive rung;
- bind the executable generation-register packet and capacity evaluator to the Lean completion used by the all-rung arithmetic theorem;
- independently replay that universal membership theorem;
- if the complete source class retains the identity completion, record the resulting complete-class nonidentifiability theorem; otherwise construct a target-clean source selector and prove its admissibility;
- prove an exact finite-size slack law with one regulator-stable physical zero for any proposed selector;
- independently certify the horizon-record, EW/Higgs load-carrier, and operational-resolution bridges;
- supply public hardware-realization evidence if a carrier implementation is claimed.
python3 -m pytest test_correctable_public_record_capacity.py -q
python3 -m pytest test_public_record_csp.py -q
python3 -m pytest test_reversible_public_checkpoint_packet.py -q
python3 -m pytest test_source_derived_public_checkpoint_packet.py -q
python3 -m pytest test_capacity_indexed_source_family.py -q
python3 -m pytest test_complete_packet_capacity_lift.py -q
python3 -m pytest test_direct_n_closure_verdict.py -q
python3 -m pytest test_horizon_record_attachment_verdict.py -q
python3 -m pytest test_operational_readback_contract.py -q
python3 -m pytest test_public_record_capacity.py -q