ScalarCurvature
plain-language theorem explainer
ScalarCurvature packages the Ricci scalar as a single real number R in the RRF ledger model of gravity. Researchers reducing tensor curvature to a scalar strain proxy cite it when mapping constraint pressure to geometric effects. The definition is a direct structure wrapper with a single field and no computation.
Claim. The scalar curvature is represented by a real number $R$, serving as a monotonic function of strain in the simplified scalar model where curvature equals constraint pressure from ledger balancing.
background
The RRF module treats gravity as the geometric manifestation of ledger constraint density, with mass as transaction density per volume and curvature as the resulting pressure when particles balance ledgers simultaneously. ScalarCurvature supplies the target type for this mapping, contrasting the full tensor of general relativity with a single real scalar. It rests on the upstream PrimitiveDistinction.from result, which extracts four structural conditions plus three definitional facts from seven independent axioms.
proof idea
The declaration is a direct structure definition introducing a single field R of type real. No lemmas or tactics are invoked; it functions as a one-line wrapper that declares the type for downstream curvature mappings.
why it matters
ScalarCurvature supplies the codomain for curvatureFromStrain, which sets R equal to kappa times the J-cost of local strain and thereby realizes the module claim that gravity is collective ledger strain. It advances the Recognition Science reduction of geometric effects to ledger constraints, consistent with the phi-ladder and eight-tick octave structures. The definition closes the simplified scalar bridge while leaving the full tensorial case open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.