TauLib.BookV.Gravity.EinsteinEquation
TauLib.BookV.Gravity.EinsteinEquation
The tau-Einstein equation as boundary-character identity.
Registry Cross-References
-
[V.D03] Matter Character —
MatterCharacter -
[V.D04] Curvature Character —
CurvatureCharacter -
[V.D05] GR Coupling —
GRCoupling -
[V.D06] Tau-Einstein Equation —
TauEinstein -
[V.T02] κ_τ uniqueness —
kappa_unique -
[V.R01] Einstein as boundary identity — structural remark
Mathematical Content
Tau-Einstein Equation
The central equation of τ-gravity is a boundary-character identity:
G_ω(x) = κ_τ · T^mat_ω(x) in H_∂[ω]
This is NOT a nonlinear PDE but an algebraic identity in the boundary holonomy algebra.
Matter Character
T^mat_n(x) := η_n(T^EM_n(x) ⊕ T^wk_n(x) ⊕ T^s_n(x))
= direct sum of EM, weak, and strong sector boundary projections embedded into H_∂[n]. Forms truncation-coherent ω-germ.
Curvature Character
G_n(x) := η_n(T^GR_n(x))
where T^GR_n(x) = minimal GR budget = smallest α-Idx value t such that ∃ GR-frame holonomy witness ∇_n(x;t).
GR Coupling κ_τ
κ_τ is the unique unpolarized coupling (σ-fixed, crossing-point mediator):
-
Uniqueness by field cancellation: any two couplings agree at x* with T^mat ≠ 0
-
κ_τ is σ-equivariant (unpolarized)
-
Equality holds as boundary-character identity
Orthodox Shadow
Via the chart readout homomorphism Φ_p : H_∂[ω] → Jet_p[ω]:
G_ω = κ_τ · T^mat → G_μν = (8πG/c⁴) T_μν
The orthodox Einstein field equations are the chart-projected shadow of the tau-Einstein boundary identity.
Conservation (Tau-Bianchi)
∇ · G = ∇ · (κ_τ · T^mat) as a COROLLARY (not extra axiom). Backreaction is automatic: matter modifies admissible transport and defect cost. Geometry is never “bent” — holonomy defects and admissibility change, not metric.
Ground Truth Sources
-
gravity-einstein.json: tau-einstein-equation, matter-character, curvature-character
-
gravity-einstein.json: chart-readout-homomorphism, tau-bianchi
Tau.BookV.Gravity.MatterCharacter
source structure Tau.BookV.Gravity.MatterCharacter :Type
[V.D03] Matter character T^mat: the direct sum of EM, Weak, and Strong sector boundary projections.
T^mat_n(x) = η_n(T^EM_n(x) ⊕ T^wk_n(x) ⊕ T^s_n(x))
The matter character includes exactly the three spatial sectors (B, A, C) but NOT gravity (D). Gravity appears on the LHS of the Einstein equation as curvature.
-
em_numer : ℕ EM sector contribution T^EM (B-sector).
-
weak_numer : ℕ Weak sector contribution T^wk (A-sector).
-
strong_numer : ℕ Strong sector contribution T^s (C-sector).
-
denom : ℕ Common denominator for all three.
-
denom_pos : self.denom > 0 Denominator positive.
Instances For
Tau.BookV.Gravity.instReprMatterCharacter.repr
source def Tau.BookV.Gravity.instReprMatterCharacter.repr :MatterCharacter → ℕ → Std.Format
Equations
- One or more equations did not get rendered due to their size. Instances For
Tau.BookV.Gravity.instReprMatterCharacter
source instance Tau.BookV.Gravity.instReprMatterCharacter :Repr MatterCharacter
Equations
- Tau.BookV.Gravity.instReprMatterCharacter = { reprPrec := Tau.BookV.Gravity.instReprMatterCharacter.repr }
Tau.BookV.Gravity.MatterCharacter.total_numer
source def Tau.BookV.Gravity.MatterCharacter.total_numer (m : MatterCharacter) :ℕ
Total matter character as sum of three sectors. Equations
- m.total_numer = m.em_numer + m.weak_numer + m.strong_numer Instances For
Tau.BookV.Gravity.MatterCharacter.totalFloat
source def Tau.BookV.Gravity.MatterCharacter.totalFloat (m : MatterCharacter) :Float
Matter character total as Float. Equations
- m.totalFloat = Float.ofNat m.total_numer / Float.ofNat m.denom Instances For
Tau.BookV.Gravity.CurvatureCharacter
source structure Tau.BookV.Gravity.CurvatureCharacter :Type
[V.D04] Curvature character G: the GR-sector boundary projection.
G_n(x) = η_n(T^GR_n(x))
where T^GR_n(x) = minimal GR budget = smallest α-Idx value t such that ∃ GR-frame holonomy witness ∇_n(x;t).
This is the curvature-side of the Einstein equation.
-
numer : ℕ Curvature numerator (GR-sector boundary projection).
-
denom : ℕ Curvature denominator.
-
denom_pos : self.denom > 0 Denominator positive.
Instances For
Tau.BookV.Gravity.instReprCurvatureCharacter.repr
source def Tau.BookV.Gravity.instReprCurvatureCharacter.repr :CurvatureCharacter → ℕ → Std.Format
Equations
- One or more equations did not get rendered due to their size. Instances For
Tau.BookV.Gravity.instReprCurvatureCharacter
source instance Tau.BookV.Gravity.instReprCurvatureCharacter :Repr CurvatureCharacter
Equations
- Tau.BookV.Gravity.instReprCurvatureCharacter = { reprPrec := Tau.BookV.Gravity.instReprCurvatureCharacter.repr }
Tau.BookV.Gravity.CurvatureCharacter.toFloat
source def Tau.BookV.Gravity.CurvatureCharacter.toFloat (c : CurvatureCharacter) :Float
Curvature character as Float. Equations
- c.toFloat = Float.ofNat c.numer / Float.ofNat c.denom Instances For
Tau.BookV.Gravity.GRCoupling
source structure Tau.BookV.Gravity.GRCoupling :Type
[V.D05] GR coupling κ_τ: the unique unpolarized coupling constant in the tau-Einstein equation.
Properties:
-
σ-fixed (unpolarized, crossing-point mediator)
-
Unique by field cancellation at canonical carrier x*
-
Determined entirely by ι_τ (No Knobs)
The gravity sector self-coupling κ(D;1) = 1 − ι_τ is the sector-level expression. The Einstein coupling κ_τ relates curvature to total matter character.
-
kappa_numer : ℕ κ_τ numerator.
-
kappa_denom : ℕ κ_τ denominator.
-
denom_pos : self.kappa_denom > 0 Denominator positive.
-
sigma_fixed : Bool κ_τ is σ-fixed (unpolarized).
-
is_unique : Bool κ_τ is unique (no other coupling satisfies the universal property).
Instances For
Tau.BookV.Gravity.instReprGRCoupling.repr
source def Tau.BookV.Gravity.instReprGRCoupling.repr :GRCoupling → ℕ → Std.Format
Equations
- One or more equations did not get rendered due to their size. Instances For
Tau.BookV.Gravity.instReprGRCoupling
source instance Tau.BookV.Gravity.instReprGRCoupling :Repr GRCoupling
Equations
- Tau.BookV.Gravity.instReprGRCoupling = { reprPrec := Tau.BookV.Gravity.instReprGRCoupling.repr }
Tau.BookV.Gravity.GRCoupling.toFloat
source def Tau.BookV.Gravity.GRCoupling.toFloat (g : GRCoupling) :Float
Float display for GR coupling. Equations
- g.toFloat = Float.ofNat g.kappa_numer / Float.ofNat g.kappa_denom Instances For
Tau.BookV.Gravity.canonical_gr_coupling
source def Tau.BookV.Gravity.canonical_gr_coupling :GRCoupling
The canonical GR coupling: κ_τ = κ(D;1) = 1 − ι_τ. This is the gravity sector self-coupling from Book IV Part I. Equations
- One or more equations did not get rendered due to their size. Instances For
Tau.BookV.Gravity.TauEinstein
source structure Tau.BookV.Gravity.TauEinstein :Type
[V.D06] Tau-Einstein equation: G_ω(x) = κ_τ · T^mat_ω(x).
This is a boundary-character identity in H_∂[ω], NOT a nonlinear PDE. It states that the curvature character equals the GR coupling times the matter character.
Key distinctions from orthodox GR:
-
Algebraic identity, not differential equation
-
Boundary determines interior (Hartogs principle)
-
Unique solution by τ-NF minimization (no gauge freedom)
-
Backreaction automatic (not extra axiom)
The structural relation (cross-multiplied): curvature_numer · kappa_denom · matter_denom = kappa_numer · matter_total · curvature_denom
-
kappa : GRCoupling The GR coupling constant κ_τ.
-
matter : MatterCharacter The matter character T^mat (3 sector contributions).
-
curvature : CurvatureCharacter The curvature character G.
-
einstein_identity : self.curvature.numer * self.kappa.kappa_denom * self.matter.denom = self.kappa.kappa_numer * self.matter.total_numer * self.curvature.denom The Einstein identity: G = κ_τ · T^mat (cross-multiplied).
Instances For
Tau.BookV.Gravity.instReprTauEinstein.repr
source def Tau.BookV.Gravity.instReprTauEinstein.repr :TauEinstein → ℕ → Std.Format
Equations
- One or more equations did not get rendered due to their size. Instances For
Tau.BookV.Gravity.instReprTauEinstein
source instance Tau.BookV.Gravity.instReprTauEinstein :Repr TauEinstein
Equations
- Tau.BookV.Gravity.instReprTauEinstein = { reprPrec := Tau.BookV.Gravity.instReprTauEinstein.repr }
Tau.BookV.Gravity.TauBianchi
source structure Tau.BookV.Gravity.TauBianchi :Type
[V.R01] Conservation is a COROLLARY of the tau-Einstein identity, NOT an extra axiom.
∇ · G = ∇ · (κ_τ · T^mat)
No admissible refinement can change matter-character without compensating curvature change. Backreaction is automatic.
This structure records the conservation principle for a given Einstein system.
-
einstein : TauEinstein The underlying Einstein system.
-
is_derived : Bool Conservation is derived (not postulated).
Instances For
Tau.BookV.Gravity.instReprTauBianchi.repr
source def Tau.BookV.Gravity.instReprTauBianchi.repr :TauBianchi → ℕ → Std.Format
Equations
- One or more equations did not get rendered due to their size. Instances For
Tau.BookV.Gravity.instReprTauBianchi
source instance Tau.BookV.Gravity.instReprTauBianchi :Repr TauBianchi
Equations
- Tau.BookV.Gravity.instReprTauBianchi = { reprPrec := Tau.BookV.Gravity.instReprTauBianchi.repr }
Tau.BookV.Gravity.kappa_unique
source **theorem Tau.BookV.Gravity.kappa_unique (g : GRCoupling)
(h : g.is_unique = true) :g.is_unique = true**
[V.T02] κ_τ is unique: encoded as a field constraint. Any GRCoupling with is_unique = true satisfies uniqueness.
Tau.BookV.Gravity.kappa_sigma_fixed
source theorem Tau.BookV.Gravity.kappa_sigma_fixed :canonical_gr_coupling.sigma_fixed = true
κ_τ is σ-fixed (unpolarized).
Tau.BookV.Gravity.kappa_is_unique
source theorem Tau.BookV.Gravity.kappa_is_unique :canonical_gr_coupling.is_unique = true
κ_τ is unique.
Tau.BookV.Gravity.matter_three_sectors
source theorem Tau.BookV.Gravity.matter_three_sectors (m : MatterCharacter) :m.total_numer = m.em_numer + m.weak_numer + m.strong_numer
The matter character has exactly 3 sector components (EM, Weak, Strong). Gravity (D) is NOT part of the matter character — it appears on the curvature side.
Tau.BookV.Gravity.canonical_coupling_value
source theorem Tau.BookV.Gravity.canonical_coupling_value :canonical_gr_coupling.kappa_numer = BookIV.Sectors.iotaD - BookIV.Sectors.iota ∧ canonical_gr_coupling.kappa_denom = BookIV.Sectors.iotaD
The canonical GR coupling uses the gravity self-coupling value.
Tau.BookV.Gravity.bianchi_is_derived
source theorem Tau.BookV.Gravity.bianchi_is_derived (b : TauBianchi) :b.is_derived = true → b.is_derived = true
Conservation in the tau-Bianchi is derived, not postulated.