capacity_readback

Correctable Public-Record Capacity

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.

Canonical lane

• F_READBACK_SPEC.md is 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.py evaluates 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.py is 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 exploring 24^12 assignments.
• test_correctable_public_record_capacity.py covers saturation, cyclic permutation, joint-coupling nonidentifiability, approximate capacity, ambiguous fibers, order countermodels, target taint, and carrier failures.
• reversible_public_checkpoint_packet.py retains the finite twelve-port icosahedral reference control. It verifies every checkpoint generator is a permutation, certifies M_0(q)=|X_reach(q)|, and emits exact rank-one saturation. It remains explicitly nonphysical.
• test_reversible_public_checkpoint_packet.py checks the 12 vertices, 30 interfaces, exact reversible capacity identity, noninjective failure, and target-taint failure.
• source_derived_public_checkpoint_packet.py defines 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, so D=|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 C2 joint 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 <= 24 and exact saturation M_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.py checks the full issue #548 acceptance surface.
• ISSUE_548_SOLUTION.md maps every acceptance item to the executable receipt.
• capacity_indexed_source_family.py generates 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.md states the bounded counterfamily theorem and its boundary. The all-rung fixed-set disagreement is also proved in Lean/ObserverPatchHolography/CapacityNonidentifiability.lean.
• direct_n_closure_verdict.py consumes that result in the direct global proposal and records that no numeric cosmic value or cosmological comparison is permitted.
• public_record_capacity.py and 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.

Generate the issue #548 receipts

python3 source_derived_public_checkpoint_packet.py --output-dir runtime

This writes the complete terminal-fiber manifest, public checkpoint packet, and certificate as canonical JSON.

Independent geometric estimator

• operational_readback_contract.py evaluates frozen scale-discrimination errors, preserves pre/post-checkpoint accounting, requires complete-fiber agreement for rho_op, and compares log M_0 with pi/rho_op^2 only after direct capacity exists.
• test_operational_readback_contract.py checks 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.

Downstream bridges

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_star with A/(4 ell_star^2) and yield Lambda 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.

Archived lanes

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.

Required completion work

• 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.

Usage

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