Encyclopedia Foundation Foundation Pair Kernel Dimensioned Hamiltonian Compiler Source Density Non Id Em

ARTICLE 3 claims 3 theorems

Foundation Pair Kernel Dimensioned Hamiltonian Compiler Source Density Non Id Em

Two different ways to attach a quantum field to a Hamiltonian produce the same physics, so the framework's current package cannot tell them apart.

Verify this page

A coupling that stays ambiguous

In quantum mechanics, a Hamiltonian is the operator that dictates how a quantum state evolves in time. The Recognition Science framework builds such Hamiltonians from a discrete ledger, a record of recognition events, by attaching a Green field to a one-body potential. The attachment uses two adjustable numbers: a potential scale and a field normalization. The framework's machine-checked library of formal theorems proves that the physics depends only on their product, the source-density coupling, and not on how that product is split between the two factors.

The theorem named emissionFD2Shadow_coupling_ne_half establishes a concrete consequence: two specific emissions, one using a field normalization of 8π and the other using 4π, produce different source-density couplings. Because the Hamiltonian's diagonal entries depend on that coupling, the two emissions also produce different Hamiltonians. The difference is real and provable, not a rounding artifact. The theorem is a formal proof in the framework's library, checked by a machine, with no unproved assumptions added.

The deeper point is non-identifiability. The framework's current package cannot decide which emission is the right one. Both emissions preserve the same surface of properties: the same event structure, a Hermitian matrix, a Stone unitary group, and a scalar energy expansion. The theorem s28_fd2_surface_does_not_select_sourceDensityCoupling packages this: it proves that the surface admits two semantics-preserving emissions with distinct couplings and distinct diagonal Hamiltonians. The separate potentialScale and fieldNormalization knobs are pure redundancy, since only their product enters the physics.

In Recognition Science, this is an honest boundary marker. The framework does not claim to have derived the source-to-density coupling from its axioms. It does not fit hydrogen or CODATA values, and it does not identify the coupling with the fine-structure constant α. The 8π factor is described as algebraic glue from a half-source Green shape to a Coulomb profile, not as a forced compiler coefficient. The theorem's role is to say what is not yet selected, so future work knows exactly which question remains open.

THEOREM emissionFD2Shadow_coupling_ne_half · IndisputableMonolith/Foundation/PairKernelDimensionedHamiltonianCompilerSourceDensityNonId.lean
emissionFD2Shadow_coupling_ne_half · IndisputableMonolith/Foundation/PairKernelDimensionedHamiltonianCompilerSourceDensityNonId.lean:87 
theorem emissionFD2Shadow_coupling_ne_half :
    emissionFD2Shadow.coupling ≠ emissionHalfGreenFactor.coupling := by
  intro h
  have hπ : (4 : ℝ) * Real.pi ≠ 0 :=
    mul_ne_zero (by norm_num) Real.pi_ne_zero
  have h' : (1 : ℝ) * (8 * Real.pi) = 1 * (4 * Real.pi) := by
    simpa [SourceDensityCouplingEmission.coupling, sourceDensityCoupling,
      emissionFD2Shadow, emissionHalfGreenFactor] using h
  have : (4 : ℝ) * Real.pi = 0 := by linarith
  exact hπ this
THEOREM potentialScale_fieldNormalization_product_redundancy · oneBodyEvolution3_product_redundancy · IndisputableMonolith/Foundation/PairKernelDimensionedHamiltonianCompilerSourceDensityNonId.lean
potentialScale_fieldNormalization_product_redundancy · IndisputableMonolith/Foundation/PairKernelDimensionedHamiltonianCompilerSourceDensityNonId.lean:110 
/-- Rescaling the two MODEL knobs with reciprocal factors leaves the potential
term unchanged. -/
theorem potentialScale_fieldNormalization_product_redundancy
    (event : PostingPair3 3)
    (potentialScale fieldNormalization zeroReference c : ℝ)
    (hc : c ≠ 0)
    (i : Fin (TorusCard3 3)) :
    (c * potentialScale) *
        q1AtomicModelPotential3 event (fieldNormalization / c) zeroReference i =
      potentialScale *
        q1AtomicModelPotential3 event fieldNormalization zeroReference i := by
  unfold q1AtomicModelPotential3
  field_simp [hc]
oneBodyEvolution3_product_redundancy · IndisputableMonolith/Foundation/PairKernelDimensionedHamiltonianCompilerSourceDensityNonId.lean:144 
/-- Reciprocal rescaling of the two knobs yields identical matrix entries. -/
theorem oneBodyEvolution3_product_redundancy
    (event : PostingPair3 3)
    (kineticScale potentialScale fieldNormalization zeroReference c : ℝ)
    (hc : c ≠ 0)
    (i j : Fin (TorusCard3 3)) :
    (oneBodyEvolution3 kineticScale (c * potentialScale)
        (q1AtomicModelPotential3 event (fieldNormalization / c)
          zeroReference)).hamiltonian i j =
      (oneBodyEvolution3 kineticScale potentialScale
        (q1AtomicModelPotential3 event fieldNormalization
          zeroReference)).hamiltonian i j := by
  rw [oneBodyEvolution3_depends_on_sourceDensityCoupling,
    oneBodyEvolution3_depends_on_sourceDensityCoupling]
  unfold sourceDensityCoupling
  field_simp [hc]
THEOREM s28_fd2_surface_does_not_select_sourceDensityCoupling · IndisputableMonolith/Foundation/PairKernelDimensionedHamiltonianCompilerSourceDensityNonId.lean
s28_fd2_surface_does_not_select_sourceDensityCoupling · IndisputableMonolith/Foundation/PairKernelDimensionedHamiltonianCompilerSourceDensityNonId.lean:304 
/-- Master non-identifiability: the S28 export and FD2 surface admit two
semantics-preserving compiler emissions with distinct source-density
couplings, and the corresponding Hamiltonians differ on the diagonal. -/
theorem s28_fd2_surface_does_not_select_sourceDensityCoupling :
    Nonempty CanonicalSourceGreenExport3 ∧
      ∃ event : PostingPair3 3,
        event ∈ realizedPrimitivePostingPairs3 3 ∧
          EmissionPreservesFD2Surface event emissionFD2Shadow ∧
            EmissionPreservesFD2Surface event emissionHalfGreenFactor ∧
              emissionFD2Shadow.coupling ≠
                emissionHalfGreenFactor.coupling ∧
                RecognitionOneBodyQuantumAttachment3
                  (oneBodyEvolution3 emissionFD2Shadow.kineticScale
                    emissionFD2Shadow.potentialScale
                    (q1AtomicModelPotential3 event
                      emissionFD2Shadow.fieldNormalization
                      emissionFD2Shadow.zeroReference)) ∧
                  RecognitionOneBodyQuantumAttachment3
                    (oneBodyEvolution3 emissionHalfGreenFactor.kineticScale
                      emissionHalfGreenFactor.potentialScale
                      (q1AtomicModelPotential3 event
                        emissionHalfGreenFactor.fieldNormalization
                        emissionHalfGreenFactor.zeroReference)) ∧
                    ∃ i : Fin (TorusCard3 3),
                      (oneBodyEvolution3 (1 / 2) 1
                          (q1AtomicModelPotential3 event (8 * Real.pi) 0)).hamiltonian
                        i i ≠
                        (oneBodyEvolution3 (1 / 2) 1
                          (q1AtomicModelPotential3 event (4 * Real.pi) 0)).hamiltonian
                        i i := by
  refine ⟨canonicalSourceGreenExport3, ?_⟩
  obtain ⟨event, hevent⟩ := realizedPrimitivePostingPair3_exists
  refine ⟨event, hevent, ?_, ?_, emissionFD2Shadow_coupling_ne_half, ?_, ?_, ?_⟩
  · exact emission_preserves_fd2_surface event hevent emissionFD2Shadow
  · exact emission_preserves_fd2_surface event hevent emissionHalfGreenFactor
  · exact emission_witnesses_attachment event hevent emissionFD2Shadow
  · exact emission_witnesses_attachment event hevent emissionHalfGreenFactor
  · exact
      distinct_sourceDensityCoupling_distinct_diagonal event hevent (1 / 2) 0
        (8 * Real.pi) (4 * Real.pi) (by
          intro h
          have hπ : (4 : ℝ) * Real.pi ≠ 0 :=
            mul_ne_zero (by norm_num) Real.pi_ne_zero
          have : (4 : ℝ) * Real.pi = 0 := by linarith
          exact hπ this)

What this page does not claim

The framework derives the source-density coupling from its axioms. The 8π factor is a forced or uniquely selected compiler coefficient. The theorem identifies the coupling with the fine-structure 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/PairKernelDimensionedHamiltonianCompilerSourceDensityNonId.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