Masses Mass Genesis T10 R4 Independence Certificate Doubled Emission World Viola

The independence certificate

The declaration doubledEmissionWorld_violates_r4 is a formal proof, checked by a machine, that a proposed rule called R4 fails in a deliberately constructed world. R4 is the rule that every realized pattern must select a single ground state. The world in question, the doubled emission world, is built from patterns that satisfy all five permitted premises of the framework, yet it contains a pattern with a doubled display, which directly contradicts R4. The proof establishes that R4 is false on the full emission envelope, meaning the rule cannot be derived from the premises alone.

The declaration is one half of an independence certificate. The other half, factorPostingWorld_satisfies_r4, constructs a different world, also satisfying the same five premises, where R4 holds. Together, the two worlds form a witness pair. The theorem r4_witness_pair_independence states that there exists a permitted-premises world where R4 fails and a permitted-premises world where R4 holds. This proves that the permitted premises do not decide R4; the rule is independent of them. The certificate does not say R4 is false everywhere, only that it is not forced by the premises.

The certificate is parametric over an arbitrary settled octave, a structure that represents a settled ledger state. This means the result holds for any such octave, not just a single example. The proof uses no unproven assumptions, no sorry, and no new axioms. It composes two previously established theorems into a new declaration. The library's own hypotheses that assume R4, such as genesis_closure_fires, are therefore hypotheses the library itself can disprove, and any conclusions drawn from them stand only as models, not as theorems.

What the declaration does not claim is equally important. It does not claim that a set-theoretic model of the entire library exists; Lean cannot internally model its own foundation. It does not claim that R4 is false in the actual universe, only that it fails in a specific constructed world. It does not claim that the missing law that would decide R4 has been found. The certificate names the exact residual: membership in the factor-posting sub-class, where patterns post at their topology factor. That missing law, factor-scale membership of creation, remains the campaign residual, a target for future work, not a result of this proof.

theorem doubledEmissionWorld_violates_r4 (octave : Q3SettledLedgerOctave) :
    ¬ RecognitionGroundStateSelection (doubledEmissionWorld octave).Realized :=
  emittedReadoutRealized_violates_r4 octave

/-- **R4 is false on the full emission envelope.** The doubled display of the
intended gap-one carrier is a member of the envelope
(`doubledCarrier_realized`) and any class containing it violates R4
(`doubled_intended_carrier_violates_r4`). Both parts are axiom-audited; the
composition is stated here for the first time. -/
theorem emittedReadoutRealized_violates_r4 (octave : Q3SettledLedgerOctave) :
    ¬ RecognitionGroundStateSelection EmittedReadoutRealized :=
  doubled_intended_carrier_violates_r4 octave EmittedReadoutRealized
    (doubledCarrier_realized _)

/-- **R4 witness-pair independence.** Over any settled octave there is a
permitted-premises world where R4 fails and a permitted-premises world where
R4 holds. The permitted premises therefore do not decide R4 in the only
sense the library can certify; what decides it is exactly the missing law
(factor-scale membership of creation), which is the campaign residual. -/
theorem r4_witness_pair_independence (octave : Q3SettledLedgerOctave) :
    (∃ w : PermittedPremiseWorld,
      ¬ RecognitionGroundStateSelection w.Realized) ∧
    (∃ w : PermittedPremiseWorld,
      RecognitionGroundStateSelection w.Realized) :=
  ⟨⟨doubledEmissionWorld octave, doubledEmissionWorld_violates_r4 octave⟩,
    ⟨factorPostingWorld octave, factorPostingWorld_satisfies_r4 octave⟩⟩

theorem t10R4IndependenceCert : T10R4IndependenceCert where
  envelope_refutes_r4 := emittedReadoutRealized_violates_r4
  negative_witness := fun octave =>
    ⟨doubledEmissionWorld octave, doubledEmissionWorld_violates_r4 octave⟩
  positive_witness := fun octave =>
    ⟨factorPostingWorld octave, factorPostingWorld_satisfies_r4 octave⟩

What this page does not claim

The certificate does not claim a set-theoretic model of the whole library exists. The certificate does not claim R4 is false in the actual universe. The certificate does not claim the missing law that would decide R4 has been found.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/MassGenesis/T10R4IndependenceCertificate.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: