Foundation Pair Kernel Gap2a Source Calorimeter Faithful Readout Interface Shape

The interface shape alone

In the Recognition Science framework, a central goal is to show that a particular physical constant, the native action quantum, is forced to equal φ⁵, the fifth power of the golden ratio. The framework's machine-checked library of formal theorems proves this under a specific set of physical assumptions. But a theorem in that library, interfaceShape_without_faithfulness_admits_candidateA, establishes a boundary on that claim: the shape of the equation alone, without the faithfulness condition, admits a different, rejected candidate value.

The theorem states that there exists a gain function and a source scale such that the source scale equals the gain at a certain dimension, yet the product of that source scale with the reduced Planck constant is not equal to one. In plainer terms, if you only look at the form of the relationship between a source scale and a readout gain, and you do not require the readout to be faithful, then you can find a configuration where the source scale is 1, not φ⁵. This configuration is the candidate A value, which the framework's other theorems reject as the correct physical scale.

What this theorem does not claim is that the interface equation shape alone is a valid physical law. The library explicitly proves the opposite in a companion theorem, interfaceShape_alone_is_not_productLaw, which shows that the shape alone permits the product to differ from 1. The faithfulness condition, which requires the readout to undo the attenuation of the channel, is what rules out such configurations. The theorem is a negative result: it clarifies that the physical content comes from the faithfulness requirement, not from the bare algebraic form of the interface.

This matters because it draws a precise line between what is derived and what is assumed. The framework does not claim that any equation of this shape forces the correct constant. It claims that a faithful readout, one that exactly reverses the channel's attenuation, forces the constant. The theorem under discussion is the guard that prevents overclaiming: it shows that without faithfulness, the door is open to the wrong answer, and therefore faithfulness is an essential, non-optional ingredient.

/-- The interface equation shape without faithfulness admits candidate A:
an unconstrained instrument datum can read one.  The selective content
lives entirely in the faithfulness law, not in the equation shape. -/
theorem interfaceShape_without_faithfulness_admits_candidateA :
    ∃ gain : ℕ → ℝ,
      candidateA_sourceMagnitudeExpr.eval =
          gain (GapDerivation.configDim GapDerivation.D) ∧
        ¬ RemainingPhysicalEquality
            candidateA_sourceMagnitudeExpr.eval :=
  ⟨fun _ => 1,
    by rw [candidateA_sourceMagnitude_eq_one],
    remainingPhysicalEquality_rejects_candidateA⟩

/-- The interface equation shape is not the killed product law: with an
unconstrained instrument, a scale reading its gain need not satisfy
`S·ħ = 1`.  Distinguishes this premise from the gate-killed
PhysicsColumnSourceCoupling proposal. -/
theorem interfaceShape_alone_is_not_productLaw :
    ∃ (gain : ℕ → ℝ) (sourceScale : ℝ),
      sourceScale = gain (GapDerivation.configDim GapDerivation.D) ∧
        sourceScale * Constants.hbar ≠ 1 :=
  ⟨fun _ => 1, 1, rfl, by
    rw [one_mul]
    exact ne_of_lt Constants.hbar_lt_one⟩

/-- **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

What this page does not claim

The interface equation shape without faithfulness is a valid physical law. The theorem proves that the native action quantum is forced to φ⁵ without additional physical assumptions. The existence of a gain function in the theorem corresponds to a physically realizable instrument.

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: