Encyclopedia Foundation Foundation Pair Kernel Gap2a Source Calorimeter Faithful Readout Readout Heat Re

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Gap2a Source Calorimeter Faithful Readout Readout Heat Re

A machine-checked theorem shows that a faithful readout of an attenuating channel can never have unit gain, ruling out a candidate quantum of heat without ever computing the golden ratio.

Verify this page

The readout's rejection of unit gain

A recognition event, a discrete record of an occurrence, can carry a block of energy through a channel that attenuates it. A faithful channel readout is an instrument that multiplies the attenuated block by a gain to recover the original reading at the channel's start. The theorem readoutHeat_rejects_unit_quantum_of_pos_dimension states that if the channel has positive dimension, meaning it actually carries something, then the readout's heat observable cannot have a quantum of exactly one. The proof never evaluates the golden ratio φ and never cites that 1 ≠ φ⁵; it holds for every attenuation constant.

The argument is purely structural. A faithful readout must undo attenuation, so its gain is the reciprocal of the block energy. The block energy at any positive step is strictly less than one, a fact that follows from the fixed point e = 1/(1+e) with e > 0. Therefore the gain is strictly greater than one. A gain of exactly one would mean the channel did not attenuate, contradicting the definition of a faithful readout. The dimension enters only as nonemptiness: the theorem requires the carrier dimension to be positive, so the block is nonempty.

In Recognition Science, the framework models this as a forced conversion quantum. The readout's gain on a complete carrier is proved to equal nativeActionQuantumInv = φ⁵, the inverse of the native action quantum, and the readout heat observable selects exactly that quantum while rejecting the unit quantum. The exclusion is value-free in the arithmetic sense: it does not depend on which constant the attenuation actually is.

What the theorem does not claim is broader. It does not establish that the source scale equals the readout gain; that identification is a separate supplied premise, SourceScaleReadsCompleteCarrierReadout, which is a HYPOTHESIS as a physical selection. The instrument laws alone do not force the remaining physical equality, and the interface shape without faithfulness admits the candidate-A quantum. The readout heat observable is defined as scaled posted flux, so its flux-proportionality itself is not derived; only its quantum is instrument-forced and candidate-A-selective.

THEOREM gain_gt_one_of_attenuating · IndisputableMonolith/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.lean
gain_gt_one_of_attenuating · IndisputableMonolith/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.lean:253 
/-- **Mechanical candidate-A exclusion.**  A faithful readout of any
nonempty block must strictly amplify: the carrier attenuates, so unit gain
would misreport the posted content.  The proof never evaluates `φ` and
never cites `1 ≠ φ⁵`; it holds for every attenuation constant. -/
theorem gain_gt_one_of_attenuating
    {N : ℕ} [NeZero N]
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout : FaithfulChannelReadout channelEnergy)
    (event : RealizedPostingEvent3 N) (m : ℕ) :
    1 < readout.gain event (m + 1) := by
  have hlt := blockEnergy_succ_lt_one channelEnergy event m
  have hpos := channelEnergy.blockEnergy_pos event (m + 1)
  rw [gain_eq_inv_blockEnergy readout event (m + 1)]
  exact (one_lt_inv₀ hpos).mpr hlt
THEOREM readoutHeat_rejects_unit_quantum_of_pos_dimension · IndisputableMonolith/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.lean
readoutHeat_rejects_unit_quantum_of_pos_dimension · IndisputableMonolith/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.lean:441 
/-- **Selectivity, exclusion half (value-free form):** on any carrier of
positive dimension, the readout heat rejects the candidate-A conversion
quantum.  The contradiction is the mechanical amplification bound
(`gain_gt_one_of_attenuating`), never the arithmetic `1 ≠ φ⁵`. -/
theorem readoutHeat_rejects_unit_quantum_of_pos_dimension
    {N : ℕ} [NeZero N]
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout : FaithfulChannelReadout channelEnergy)
    (physical : PostingPhysicalChannelCarrier3 N)
    (event : RealizedPostingEvent3 N)
    (hdim : 0 < physicalPostingCarrierDimension3 physical event) :
    ¬ HeatIsPostedRecordFlux 1 (readoutHeat readout physical event) := by
  intro h
  have hq :=
    readoutHeat_quantum_unique readout physical event 1 h
  obtain ⟨m, hm⟩ :=
    Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.mp hdim)
  rw [hm] at hq
  exact gain_ne_one_of_attenuating readout event m hq.symm
THEOREM completeCarrier_gain_eq_nativeActionQuantumInv · IndisputableMonolith/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.lean
completeCarrier_gain_eq_nativeActionQuantumInv · IndisputableMonolith/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.lean:290 
/-- On a coherence-complete physical carrier, the faithful gain is exactly
the reciprocal native action quantum `φ⁵`.  The dimension `5` arrives from
the same completeness theorem arrow A used
(`completeCarrier_dimension_eq_configDim`), and the value from
`gain_forced`; neither is posited here. -/
theorem completeCarrier_gain_eq_nativeActionQuantumInv
    {N : ℕ} [NeZero N]
    {physical : PostingPhysicalChannelCarrier3 N}
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout : FaithfulChannelReadout channelEnergy)
    (hcomplete : PostingCarrierCoherenceComplete3 physical)
    (event : RealizedPostingEvent3 N) :
    readout.gain event
        (physicalPostingCarrierDimension3 physical event) =
      nativeActionQuantumInv := by
  rw [gain_forced readout event
      (physicalPostingCarrierDimension3 physical event),
    completeCarrier_dimension_eq_configDim hcomplete event,
    GapDerivation.configDim_at_D3,
    nativeActionQuantumInv_eq_constants_phi_pow_five,
    zpow_natCast]
THEOREM faithfulReadout_alone_does_not_force_remainingPhysicalEquality · IndisputableMonolith/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.lean
faithfulReadout_alone_does_not_force_remainingPhysicalEquality · IndisputableMonolith/Foundation/PairKernelGap2aSourceCalorimeterFaithfulReadout.lean:564 
/-- 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 source scale equals the readout gain is not derived; it is a supplied physical identification. The flux-proportionality of the readout heat observable is not derived; only its quantum is instrument-forced. The unit-quantum exclusion does not depend on the golden ratio or any particular attenuation constant.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND