Ilg Cpminstance Ilg Constants Pos

The positivity theorem

The theorem ilgConstants_pos establishes that three numbers attached to a model of infra-luminous gravity are all greater than zero. Those numbers are K_net, C_proj, and C_eng. K_net is a covering number, a count of how many small pieces cover a space at a given resolution; here it equals (9/7)². C_proj is a bound from a projection step, equal to 2; C_eng is an energy normalization, equal to 1. The theorem proves 0 < K_net, 0 < C_proj, and 0 < C_eng, and the proof is a direct computation from the definitions, checked by a machine.

The positivity is a small but necessary ingredient in a larger argument. The model, called ILG, is a coercive projection model: it says that a certain measure of deviation, the defect mass, is controlled by an energy gap. The control has the form defect mass ≤ (K_net · C_proj · C_eng) · energy gap. That inequality is the coercivity theorem. The positivity of the three constants is what lets the inequality be read as a genuine bound rather than a triviality: if any constant were zero or negative, the product on the right could collapse and the control would be meaningless. So the theorem is a hygiene check, a guarantee that the constants behave as a bound should.

The theorem does not claim that the ILG model is true of the real universe. It does not claim that the energy control hypothesis holds; that hypothesis is a separate assumption, stated as a predicate and not proved. It does not claim that the constants are derived from first principles; they are chosen definitions. It does not claim that the model predicts any specific rotation curve. The theorem only says: given these definitions, the three named constants are positive. That is all.

What the positivity actually buys is a clean statement of the coercivity bound. With the constants positive, the inequality defect mass ≤ (K_net · C_proj · C_eng) · energy gap is a real constraint, not a vacuous one. It is the kind of result that makes a model usable in further analysis: a bound that holds with explicit, positive coefficients. For a reader, the practical takeaway is that the ILG model passes a basic sanity check: its control constants are not degenerate. Whether the model describes galaxies is a separate question, one that the positivity theorem does not touch.

/-- Positivity of ILG constants. -/
theorem ilgConstants_pos :
    0 < ilgConstants.Knet ∧ 0 < ilgConstants.Cproj ∧ 0 < ilgConstants.Ceng := by
  refine ⟨?_, ?_, ?_⟩ <;> simp only [ilgConstants] <;> norm_num

/-- ILG-specific CPM constants derived from eight-tick geometry.
    - K_net = (9/7)² from ε = 1/8 covering
    - C_proj = 2 from J''(1) = 1 normalization
    - C_eng = 1 standard energy normalization
    - C_disp = 1 dispersion bound -/
noncomputable def ilgConstants : Constants := {
  Knet := (9/7)^2,
  Cproj := 2,
  Ceng := 1,
  Cdisp := 1,
  Knet_nonneg := by norm_num,
  Cproj_nonneg := by norm_num,
  Ceng_nonneg := by norm_num,
  Cdisp_nonneg := by norm_num
}

/-- ILG-specific CPM constants derived from eight-tick geometry.
    - K_net = (9/7)² from ε = 1/8 covering
    - C_proj = 2 from J''(1) = 1 normalization
    - C_eng = 1 standard energy normalization
    - C_disp = 1 dispersion bound -/
noncomputable def ilgConstants : Constants := {
  Knet := (9/7)^2,
  Cproj := 2,
  Ceng := 1,
  Cdisp := 1,
  Knet_nonneg := by norm_num,
  Cproj_nonneg := by norm_num,
  Ceng_nonneg := by norm_num,
  Cdisp_nonneg := by norm_num
}

/-- The coercivity theorem for ILG: energy gap controls defect mass. -/
theorem ilg_coercivity (P : KernelParams) (h_energy : EnergyControlHypothesis P) (s : ILGState) :
    (ilgModel P h_energy).defectMass s ≤
    ((ilgModel P h_energy).C.Knet * (ilgModel P h_energy).C.Cproj * (ilgModel P h_energy).C.Ceng) *
    (ilgModel P h_energy).energyGap s :=
  (ilgModel P h_energy).defect_le_constants_mul_energyGap s

/-- Energy control hypothesis: the energy of a configuration bounds its defect.
    This is the physical content of the variational principle (Lax-Milgram).
    In ILG, this states that the gravitational energy controls the deviation
    from the Newtonian solution. -/
def EnergyControlHypothesis (P : KernelParams) : Prop :=
  ∀ s : ILGState, defectMass P s ≤ energyGap s

What this page does not claim

The ILG model is a correct description of real galaxies. The constants K_net, C_proj, C_eng are derived from first principles rather than chosen. The energy control hypothesis is proved true.

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/ILG/CPMInstance.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: