Foundation Pair Kernel Gap2a Source Calorimeter Faithful Readout Source Calorime

The source calorimeter theorem

The declaration sourceCalorimeter_forces_remainingPhysicalEquality is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that if a certain physical identification holds, then a specific numerical equality, RemainingPhysicalEquality, follows. In plain terms, the theorem says: given a faithful readout of a complete carrier, and given that the source scale reads that readout, then the source scale equals the unique cotangent coordinate, which is φ⁵.

The theorem is not a free-standing proof of that equality. It depends on a premise called SourceScaleReadsCompleteCarrierReadout. This premise asserts that the source scale equals the gain of the faithful readout. The framework's own documentation calls this premise a physical identification, a hypothesis, not a derived result. The theorem proves the conditional statement: if the premise holds, then the equality follows. It does not prove the premise itself.

The framework's library also proves that the instrument laws alone do not force the equality. A separate theorem, faithfulReadout_alone_does_not_force_remainingPhysicalEquality, shows that the existence of a faithful readout is not enough to conclude the equality for all source scales. This is a deliberate honesty wall: the theorem's power is conditional on its premise.

What the theorem does establish is a structural result within the framework. It shows that the equality is not arbitrary; it is forced once the interface premise is accepted. The theorem also discharges a previously banked revival door, routing through sourceCalorimeter_discharges_landauer_revival. The framework's cold-audit verdict, however, notes that the premise is propositionally equivalent to the equality under completeness and faithfulness, so the premise does not clear the gate as a strictly weaker assumption.

In Recognition Science, this theorem is part of a campaign to derive physical constants from the framework's axioms. The theorem narrows the gap: the missing premise is no longer a bare value selection but a typed instrument interface. The law itself, however, is not derived unconditionally.

/-- **Conditional closure.**  Interface premise + faithful instrument +
coherence-complete carrier force the residual atom.  This is a theorem
about what the typed interface buys; it is not an unconditional derivation
of the adopted law. -/
theorem sourceCalorimeter_forces_remainingPhysicalEquality
    {N : ℕ} [NeZero N]
    {physical : PostingPhysicalChannelCarrier3 N}
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout : FaithfulChannelReadout channelEnergy)
    (hcomplete : PostingCarrierCoherenceComplete3 physical)
    {sourceScale : ℝ} {event : RealizedPostingEvent3 N}
    (hinterface :
      SourceScaleReadsCompleteCarrierReadout
        physical readout sourceScale event) :
    RemainingPhysicalEquality sourceScale := by
  change sourceScale = uniqueCotangentCoordinate
  exact hinterface.trans
    (completeCarrier_gain_eq_uniqueCotangentCoordinate
      readout hcomplete event)

/-- **HYPOTHESIS (physical selection; the remaining new physical input).**
The priced source covector scale reads the complete-carrier faithful
readout gain.  The text is target-blind: no `hbar`, no `φ⁵`, no cotangent
coordinate, no product law.  Honesty: given a faithful readout, this is
logically equivalent to the residual atom, because the corpus proves the
atom is otherwise undecided; adopting it is a physical identification of
the covector's reading process with the instrument, parallel in kind to
the S10/S16/S17 parents that arrow A consumed. -/
def SourceScaleReadsCompleteCarrierReadout
    {N : ℕ} [NeZero N]
    (physical : PostingPhysicalChannelCarrier3 N)
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout : FaithfulChannelReadout channelEnergy)
    (sourceScale : ℝ)
    (event : RealizedPostingEvent3 N) : Prop :=
  sourceScale =
    readout.gain event
      (physicalPostingCarrierDimension3 physical event)

/-- The instrument laws alone do not force the atom: they never mention the
source scale, so pairing them with every scale is vacuous.  Mirrors the
free-`q` countermodel of the D2 wall. -/
theorem faithfulReadout_alone_does_not_force_remainingPhysicalEquality :
    ¬ (∀ sourceScale : ℝ,
      (∃ channelEnergy : PostingEventChannelEnergy3 3,
        Nonempty (FaithfulChannelReadout channelEnergy)) →
        RemainingPhysicalEquality sourceScale) := by
  intro hforce
  exact remainingPhysicalEquality_rejects_candidateA
    (hforce candidateA_sourceMagnitudeExpr.eval
      ⟨canonicalPostingEventChannelEnergy3,
        ⟨canonicalFaithfulReadout canonicalPostingEventChannelEnergy3⟩⟩)

What this page does not claim

The theorem does not prove that the source scale equals φ⁵ unconditionally. The theorem does not discharge the MissingIndependentCellCalorimeter. The theorem does not show that the interface premise is a strictly weaker assumption than the equality it helps prove.

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/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.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: