M_max
plain-language theorem explainer
M_max defines the maximum mass from coherent assembly over N cycles at density ρ as the product of ρ, the coherence volume V_coherence, and N. Astrophysicists modeling neutron star maximum masses or stellar observability limits cite this bound when applying recognition constraints to mass assembly. The definition is a direct arithmetic product that multiplies the precomputed coherence volume by the supplied parameters.
Claim. $M_ {max}(N, ρ) = ρ · V_{coherence} · N$, where the coherence volume $V_{coherence} = l_{rec}^3$ is the maximum assembly volume fixed by the recognition length.
background
This definition sits in the Recognition-Bounded Observability module, which derives mass-to-light ratios from the requirement that photon flux exceed the recognition threshold while mass assembly stays inside the coherence volume. V_coherence is the sibling definition l_rec cubed, the maximum volume available for coherent assembly. Upstream results supply the scale function scale(k) = phi^k from LargeScaleStructureFromRS and the cost functions that assign J-cost to recognition events in ObserverForcing and MultiplicativeRecognizerL4.
proof idea
The definition is a direct product ρ * V_coherence * N. It uses the sibling definition of V_coherence as l_rec^3 and performs ordinary real multiplication; no lemmas or tactics beyond the arithmetic are required.
why it matters
M_max supplies the mass argument to IsMaximumMass in NeutronStarTOV, which locates the local maximum of the M(P_c) curve and encodes the TOV stability criterion. It implements the mass-assembly limit inside the observability strategy, connecting the coherence volume to the phi-ladder and supporting the M/L interval {phi^n : n in [0,3]} stated in the module. The definition closes the geometric-constraint portion of the derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.