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)
230theorem gap6_resolved : gap6_resolution.status = "RESOLVED_BY_LAYER_SEPARATION" := rfl
proof body
Term-mode proof.
231
232/-! ## Claim Dependencies -/
233
234/-- Claims that depend on the core integer-rung convention -/
depends on (9)
Lean names referenced from this declaration's body.
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
status
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
status
in IndisputableMonolith.Measurement.RSNative.Alignment
decl_use
-
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
gap6_resolution
in IndisputableMonolith.Physics.QuarkCoordinateReconciliation
decl_use
-
rung
in IndisputableMonolith.RSBridge.Anchor
decl_use