No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
153def status_summary : String :=
proof body
Body contains sorry. Scaffold only; not proved.
154 "U1: EffectiveManifoldHypotheses — bundles U2+U4 into single structure\n" ++
155 "U2: RefinementConverges — eventually separates all distinct points\n" ++
156 "U3: DimensionInvariant — stated as hypothesis interface\n" ++
157 "U4: NonCollapseCondition — monotone separation (auto from refinement)\n" ++
158 " monotone_separation_of_refinement: PROVED (no sorry)\n" ++
159 " convergence_implies_identity: PROVED (no sorry)\n" ++
160 "STATUS: Hypothesis interfaces complete; manifold existence is the\n" ++
161 " genuinely open mathematics (requires topology of inverse limits)."
162
163end EffectiveManifold
164end RecogGeom
165end IndisputableMonolith
depends on (24)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Hypothesis
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
complete
in IndisputableMonolith.Complexity.SAT.Backprop
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
refinement
in IndisputableMonolith.Papers.DraftV1
decl_use
-
convergence_implies_identity
in IndisputableMonolith.RecogGeom.EffectiveManifold
decl_use
-
DimensionInvariant
in IndisputableMonolith.RecogGeom.EffectiveManifold
decl_use
-
EffectiveManifoldHypotheses
in IndisputableMonolith.RecogGeom.EffectiveManifold
decl_use
-
monotone_separation_of_refinement
in IndisputableMonolith.RecogGeom.EffectiveManifold
decl_use
-
NonCollapseCondition
in IndisputableMonolith.RecogGeom.EffectiveManifold
decl_use
-
RefinementConverges
in IndisputableMonolith.RecogGeom.EffectiveManifold
decl_use