Position
plain-language theorem explainer
Position supplies the real line as the coordinate type for heights and potentials in coherence-fall gravity models. Workers on acoustic levitation, energy processing bridges, and conditional complexity results cite it when constructing fields or objects. The declaration is a direct abbreviation with no additional structure or proof steps.
Claim. Let Position stand for the real numbers $ℝ$, used as the domain for potential functions and center-of-mass coordinates.
background
In the CoherenceFall module the type Position appears as the domain of potential functions. ProcessingField packages a map phi : Position → ℝ that encodes processing potential at each coordinate. ExtendedObject records a center-of-mass height h_cm : Position together with a positive extent. ExternalPhaseField likewise carries an external contribution psi : Position → ℝ whose gradient modifies the local environment. The module imports only Mathlib, so Position inherits the standard ordered field and topology of the reals.
proof idea
Direct abbreviation: Position is introduced as ℝ with no further clauses or lemmas applied.
why it matters
The abbreviation anchors every position-dependent construction in the gravity section. It is referenced by ExternalPhaseField, ExtendedObject, EnergyDistribution, and coherence_defect lemmas inside the module, and by the conditional P ≠ NP assembly and W-mass anomaly theorems downstream. It therefore supplies the spatial coordinate required for any later statement that links coherence defects to gravitational fall or acoustic phase fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.