planckArea_pos
plain-language theorem explainer
The theorem establishes that the Planck area is strictly positive. Researchers modeling holographic bounds and recognition bandwidth cite it to keep denominators positive in rate formulas. The proof is a one-line term wrapper that unfolds planckArea and planckLength then invokes the positivity tactic.
Claim. $0 < 4ell_P^2$ where $ell_P$ is the Planck length appearing in the holographic bound $A/(4ell_P^2 cdot ln(phi) cdot 8tau_0)$.
background
The Recognition Bandwidth module connects the holographic bound (maximum information proportional to boundary area over four Planck areas), the per-bit recognition cost $k_R = ln(phi)$, the ILG parameters, and the eight-tick cadence (period $8tau_0$) to define recognition bandwidth as the maximum ledger throughput $R_max = A / (4ell_P^2 cdot ln(phi) cdot 8tau_0)$. Upstream structures supply the discrete phi-tiers (NucleosynthesisTiers), J-cost calibration (PhiForcingDerived), ledger factorization (DAlembert.LedgerFactorization), and spectral emergence of gauge content (SpectralEmergence).
proof idea
Term-mode one-liner. The proof unfolds the definitions of planckArea and planckLength to obtain an expression whose positivity is immediate, then applies the positivity tactic.
why it matters
The result supplies the positivity needed for the denominator in bandwidth_denom_pos and for the maintenanceBudget_pos theorem in ConsciousnessBandwidth. It anchors the Planck-area term inside the holographic bound formula that appears in the module's definition of $R_max$, consistent with the eight-tick octave and the forcing-chain derivation of spatial dimensions. Downstream applications invoke it directly via linarith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.