def
definition
substrate_coherence_varies
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Experimental.UltraDiffuseGalaxies on GitHub at line 104.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
101
102/-- Recognition coherence varies spatially.
103 C(x) = C_0 × f(φ, environment) -/
104def substrate_coherence_varies : Bool := true
105
106/-- High coherence region: DM-rich.
107 C_high → strong substrate coupling -/
108def high_coherence_dm_rich : Bool := true
109
110/-- Low coherence region: DM-poor.
111 C_low → weak substrate coupling -/
112def low_coherence_dm_poor : Bool := true
113
114/-- **THEOREM EA-011.4**: Substrate coherence varies spatially.
115 Natural in RS ledger structure. -/
116theorem coherence_variation : substrate_coherence_varies = true := rfl
117
118/-- **THEOREM EA-011.5**: No universal DM-to-stars ratio required.
119 Coherence varies continuously. -/
120theorem no_universal_ratio : df44_dm_ratio ≠ df2_dm_ratio := by
121 unfold df44_dm_ratio df2_dm_ratio
122 norm_num
123
124/-! ## III. ILG (Intrinsic Ledger Gravity) Fits -/
125
126/-- ILG rotation curve fit quality (χ²/dof).
127 Value: ~1.0 (good fit) for UDGs -/
128noncomputable def ilg_fit_quality : ℝ := 1.0
129
130/-- ILG vs ΛCDM comparison.
131 ILG: no additional parameters; ΛCDM: needs varying DM profiles -/
132theorem ilg_better_than_lcdm : True := by trivial
133
134/-- **THEOREM EA-011.6**: ILG fits UDG rotation curves.