pith. machine review for the scientific record. sign in

arxiv: 2506.14617 · v2 · submitted 2025-06-17 · ✦ hep-ph · hep-th

Recognition: 5 theorem links

· Lean Theorem

Inflation in the Scale Symmetric Standard Model and Weyl geometry

Z. Lalak , P. Michalak
Authors on Pith no claims yet

Pith reviewed 2026-05-06 17:46 UTC · model claude-opus-4-7

classification ✦ hep-ph hep-th
keywords Higgs inflationdilatonWeyl geometryscale invariancenon-minimal couplingone-loop effective potentialtensor-to-scalar ratiounitarity cutoff
0
0 comments X

The pith

A scale-symmetric Higgs–dilaton model in Weyl geometry yields a single-field plateau inflaton whose spectrum can match Planck/ACT, but whose unitarity cutoff sits below the inflation scale when ξ₁ ≫ ξ₀.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper asks whether the Standard Model Higgs, coupled to a singlet dilaton and embedded in Weyl conformal geometry, can drive inflation while generating all mass scales (Planck, electroweak, Higgs) from a single dilaton vev. After conformally rescaling to the Einstein frame and using polar field coordinates, the radial direction becomes pure gauge (eaten by the Weyl vector ω_μ), leaving an angular field τ as a single canonical inflaton on a plateau potential. The authors compute the one-loop effective potential including curvature terms and run the couplings using β-functions modified by propagator-suppression factors c_{φᵢ} that account for the non-canonical Einstein-frame commutators. They find parameter ranges in (ξ₀, p = ξ₁/ξ₀) where n_s and r_{0.002} can be made compatible with Planck and ACT data, with quantum corrections shifting the potential by less than an order of magnitude. The version-of-record conclusion is sober: r is small enough (≲ 10⁻⁶) to be invisible to gravitational-wave probes, and in the phenomenologically natural hierarchy ξ₁ ≫ ξ₀ the W-W scattering cutoff Λ_UV ∼ M_P/√ξ₁ lies below the inflationary energy scale, threatening the EFT validity of the construction.

Core claim

Embedding the Standard Model Higgs together with a dilaton in Weyl conformal geometry produces, after going to the Einstein frame and integrating out the (heavy) Weyl gauge boson, a single-field inflaton τ = tan θ in field-space polar coordinates, with a non-canonical kinetic function F(τ) and a potential that asymptotes to a plateau V_∞ = 36 λ₂ M_P⁴/ξ₁². Slow-roll on this plateau, with one-loop curvature-dressed corrections and propagator-suppression factors c_{φᵢ} that modify the running of couplings, can be made compatible with the measured spectral index n_s and a tensor-to-scalar ratio r_{0.002}. In the version of record, however, r_{0.002} comes out ≲ 10⁻⁶ (undetectable), and the unita

What carries the argument

A Weyl-invariant two-scalar action with non-minimal couplings ξ₀φ₀² + ξ₁φ₁², passed to the Einstein frame via Ω² = (ξ₀φ₀² + ξ₁φ₁²)/6M². In polar field coordinates the radial mode is gauged away into the Weyl vector, leaving the angular mode τ = tan θ as a single canonical inflaton with kinetic function F(τ) and plateau potential V(τ). Quantum corrections are computed in the Einstein frame using the Markkanen–Nurmi–Rajantie–Stopyra curved-space one-loop formula, while β-functions are evaluated in the Jordan frame with field-dependent renormalization scale μ(φ₀) and propagator-suppression factors c_{φᵢ} = [Ω² F²(τ) (∂φᵢ/∂τ)²]⁻¹ that enforce the non-canonical commutation relations.

If this is right

  • Mass scales (Planck mass
  • Higgs vev
  • Higgs mass) all emerge from a single dilaton vev once scale symmetry is spontaneously broken
  • with no explicit mass terms in the Lagrangian.
  • The Weyl gauge boson eats the radial mode of (φ₀
  • φ₁)
  • leaving a single physical inflaton τ
  • for q ≳ O(1) it has Planck-scale mass and decouples from inflationary dynamics.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The visible tension between the v1 abstract (r ≲ 10⁻³
  • detectable
  • cutoff safe) and the v2 abstract (r ≲ 10⁻⁶
  • undetectable
  • cutoff below the inflation scale) suggests that the consistency of the scenario hinges sharply on how the endpoint of inflation η_V(τ_end) is fixed
  • the model's predictions are not stable under O(10⁻³) shifts in that endpoint convention.
  • Because the Weyl gauge boson is taken heavy (m_ω ∼ q M_P) and decoupled
  • the analysis is effectively a Higgs-dilaton non-minimal model with extra geometric kinetic structure

Load-bearing premise

That the Weyl gauge boson can be safely treated as heavy and decoupled during inflation, so that the dynamics really collapse to a single inflaton — an approximation that breaks down precisely when the Weyl gauge coupling q is small, which is the regime where the geometric framework would otherwise be most distinctive.

What would settle it

A direct check of whether tree-level longitudinal W-boson scattering on the inflationary background actually preserves perturbative unitarity up to V(τ_*)^{1/4}: if Λ_UV = √(8π) m_W(τ_0)/(g₂/2)·1/√(R²−1) genuinely falls below the Hubble scale during slow roll for the parameter region that fits n_s, the model cannot be trusted as an effective field theory of inflation. Conversely, an observed r ≳ 10⁻⁴ in B-mode searches would rule out the version of the model in which r ≲ 10⁻⁶.

read the original abstract

This work explores the possibility of inflation in a scale-symmetric extension of the Standard Model Higgs sector, where the Higgs field $\phi_1$ is coupled to a singlet scalar, the dilaton $\phi_0$. The two-scalar theory is formulated within Weyl geometry, which modifies the Einstein frame form of the resulting single-field inflationary potential. We extend the analysis to include quantum corrections, incorporating curvature effects in the one-loop effective potential. We find that the resulting spectral index $n_s$ and tensor-to-scalar ratio $r_{0.002}$ can be consistent with the Planck 2018 observational constraints. The predicted value $r_{0.002} \lesssim 10^{-6}$ remains too small to yield a detectable gravitational wave signal. In the regime with a strong hierarchy between the non-minimal couplings, $\xi_1\ll\xi_0$, the unitarity cutoff in the large-field background, $\Lambda_{UV}\sim M_P/\sqrt{\xi_1}$, lies below the energy scales relevant during inflation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

5 major / 7 minor

Summary. The authors construct a scale-symmetric two-scalar (Higgs ϕ₁ + dilaton ϕ₀) extension of the SM in Weyl conformal geometry, transform to the Einstein frame, parametrize the inflaton in polar coordinates τ = tan θ, and analyze slow-roll inflation both classically (§3) and with a one-loop RG-improved effective potential including curvature contributions and propagator suppression factors c_{ϕᵢ} (§4). Cosmological observables (n_s, r_{0.002}) are confronted with ACT DR6 + Planck constraints, the gravitational-wave signal is computed (§4.2), and the unitarity cutoff in the inflationary background is estimated from W_L W_L scattering (§5).

Significance. If the construction is correct, the paper offers a careful integration of three ingredients — Weyl-geometric formulation, one-loop curvature corrections in the Einstein frame, and propagator-suppression-modified RG running — for Higgs-dilaton inflation, with explicit parameter-space regions and a unitarity-bound analysis at the τ_* background rather than only at the vacuum. The inclusion of the dilaton kinetic term in the Weyl framework and the explicit comparison of β-functions with and without c_{ϕᵢ} (Appendix C) are useful technical contributions. However, several internal inconsistencies (see below) currently obscure what the paper actually concludes, which limits the assessable significance of the result.

major comments (5)
  1. [Abstract vs. §5 (Eq. 5.14)] The two versions of the abstract supplied with v2 are mutually inconsistent and inconsistent with §5. The arXiv metadata abstract states 'Λ_{UV} ∼ M_P/√ξ_1 lies below the energy scales relevant during inflation' and 'r_{0.002} ≲ 10^{−6} … too small to yield a detectable gravitational wave signal,' while the in-manuscript abstract states 'r_{0.002} ≲ 10^{−3} is sufficient to yield a detectable gravitational wave signal.' §5 explicitly concludes the opposite of the metadata abstract on the cutoff: 'the cutoff exceeds the inflationary energy scale V(τ_*)^{1/4} by a factor of 11.9236, ensuring the validity of our results.' This is the load-bearing self-consistency claim of the paper; the authors must reconcile these statements and present a single, internally consistent conclusion before the inflationary observables in §3–§4 can be assessed.
  2. [§3, Eq. (3.4) and surrounding text] The endpoint of inflation is defined by η_V(τ_end) = −0.0095 (and varied in {−0.0125,…,−0.0095} in Figs. 7, 13). This is non-standard: end-of-inflation is conventionally defined by breakdown of slow-roll (ε_V → 1), and η_V at the experimental value of −0.0095 should be imposed at the horizon-crossing point τ_*, not at τ_end. As written, η_V(τ_end) functions as a tunable knob whose chosen values coincide numerically with the observational η_V at τ_*, and then n_s is reported as 'consistent with experiment' (Figs. 7, 8, 13). Please justify this prescription, demonstrate that ε_V(τ_end) ≪ 1 is acceptable physically, and clarify whether the agreement with ACT DR6 in Fig. 8 is genuine prediction or an artifact of identifying τ_end with the observational η_V threshold.
  3. [§4.2, Fig. 14] The conclusion that 'the predicted GW signal lies within the detectable range, providing a potential test' is not supported by Fig. 14a/14b as drawn. The displayed spectra correspond to r_{0.002} = 10^{−3.6}, 10^{−4.2}, 10^{−5}, with Ω_GW h² peaking near 10^{−15}–10^{−17} at LISA/ET/BBO frequencies — well below the plotted experimental sensitivity envelopes at those frequencies. The only realistically detectable channel for r ≳ 10^{−3.6} is CMB B-mode polarization at the lowest frequencies, which the authors should state explicitly. As it stands the §4.2 detectability claim and the metadata-abstract claim of undetectability point in opposite directions; one is wrong.
  4. [§2, Eq. (2.17) and decoupling assumption below Eq. (2.17)] The reduction from the two-scalar Lagrangian (2.14) to the single-field inflaton Lagrangian (2.18) relies on m_ω² ≳ (3q²/2) M_P² being above the inflation scale, justified only by the assumption q ≳ 1 and the Weak Gravity Conjecture footnote. The conclusions concede that for smaller q this approximation breaks down. Given that the paper does not derive q from any internal scale, please add a quantitative bound on q below which the ω_µ contribution to the inflaton EOM and the one-loop potential is no longer negligible, and check that the ACT-compatible parameter points used in Figs. 8, 12, 13 lie above that bound.
  5. [§4.1, Eq. (4.13)] The choice μ = H_inf with H_inf² = V_{1-loop}(τ=10², H_inf, μ_i)/(3M_P²) is implicit and self-referential. Please demonstrate that this defining equation has a unique positive solution in the parameter ranges scanned in Figs. 11–13, and that the claimed insensitivity to μ_1 vs μ_2 (≤5% in couplings) propagates to ≪ 1σ in n_s. Otherwise the comparison to V(τ) in Fig. 10 and the boundary log_{10} p ≥ −log_{10} ξ_0 + 4.2 in Fig. 11 carry hidden μ-prescription dependence.
minor comments (7)
  1. [Fig. 2 caption] Caption gives ξ_0 = 10^{15} and ξ_1 = 10^{10}, but the parameter-space analysis later (Eq. 3.6, Fig. 3b) requires log_{10} ξ_0 ≲ −1.727. Either replace the figure with a viable parameter point or clearly state that Fig. 2 is illustrative only.
  2. [Two abstracts] The v2 submission carries two textually different abstracts (the arXiv metadata abstract and the abstract printed inside the PDF). Please ensure they are identical in the next revision; the discrepancy on r_{0.002} (10^{−6} vs 10^{−3}) and on the cutoff–inflation-scale ordering is a significant source of confusion.
  3. [Table 1] The η_V row is listed in units of 10^{−4}, giving −95^{+23}_{−30}, i.e. η_V ≈ −0.0095. This is the inferred value at horizon crossing; please state explicitly that it is evaluated at τ_*, not at the inflation endpoint, to avoid confusion with the τ_end prescription used in §3.
  4. [Eq. (2.21) and Eq. (2.20)] V_∞ = 36 λ_2 M_P^4/ξ_1² is identified as the 'maximum potential energy that could be reached during inflation', but the τ → ∞ limit is asymptotic and never reached at finite τ_*. State whether the bound (2.22) is imposed at V_∞ or at V(τ_*).
  5. [§5, Eq. (5.13)–(5.14)] It would help the reader to plot Λ_UV / V(τ_*)^{1/4} as a function of (ξ_0, p) directly, since this single ratio is what determines EFT validity for the inflationary observables. Fig. 17 gives Λ_UV in units of M_P but does not display the comparison to V^{1/4} that §5 verbally invokes.
  6. [Appendix C, Eq. (C.6)] Please give a brief comment on whether the c_{ϕᵢ}-modified β-functions are gauge-invariant; for non-canonical kinetic terms the suppression factors enter through the Higgs propagator, and the gauge β-functions in (C.6) inherit a c_1-dependence that is unusual.
  7. [Footnote 2 (q ≲ 4)] The Weak Gravity Conjecture bound q ≲ 4 is asserted without citation; please cite the specific WGC variant invoked, since for massive vectors with scalar hair the relevant inequality is not unique.

Simulated Author's Rebuttal

5 responses · 1 unresolved

We thank the referee for a careful and constructive report. The referee has correctly identified that the v2 submission contains two mutually inconsistent abstracts and a related inconsistency between the §4.2 detectability statement, the §5 unitarity conclusion, and the arXiv-metadata abstract. This arose during a substantial revision in which the unitarity analysis was redone at the τ_* background (rather than only at the vacuum) and the GW prediction was re-evaluated, but the two abstracts and the §4.2 wording were not synchronized. We agree this must be fixed before the physics conclusions can be assessed, and we will issue a v3 with a single, internally consistent narrative. We also accept the referee's points on (i) the non-standard end-of-inflation prescription, (ii) the need for a quantitative bound on q controlling ω_µ decoupling, and (iii) the implicit definition of µ = H_inf. Below we respond point by point and indicate which items we will revise.

read point-by-point responses

  1. Referee: Abstract vs. §5 (Eq. 5.14): the two abstracts and §5 give mutually inconsistent statements about Λ_UV vs. the inflationary scale and about r_{0.002} (10^-6 undetectable vs. 10^-3 detectable). Reconcile.

    Authors: The referee is correct and we apologize for the confusion. The arXiv-metadata abstract is a stale fragment from an earlier draft in which (a) the unitarity bound was evaluated only at the vacuum, giving Λ_UV ~ M_P/ξ_1 below the inflation scale, and (b) the parameter scan produced r_{0.002} ≲ 10^-6. In the present analysis Λ_UV is evaluated at the inflationary background τ_* (Sec. 5, Eq. 5.14), where it exceeds V(τ_*)^{1/4} by a factor ≈ 11.92, and the scan in Figs. 12–13 yields r_{0.002} up to ~10^{-3.6}. The in-manuscript abstract reflects the current analysis. In v3 we will: (i) replace the arXiv metadata abstract with the in-manuscript one; (ii) state explicitly that the cutoff is safe in the inflationary background while the vacuum-limit cutoff Λ_UV ~ M_P/ξ_1 is parametrically lower (Eq. 5.16); (iii) restrict the GW detectability claim as discussed in our response on §4.2. revision: yes

  2. Referee: §3: defining τ_end by η_V(τ_end) = -0.0095 (and varying it) is non-standard; conventional end-of-inflation is ε_V → 1, with η_V at -0.0095 imposed at τ_*. Is the agreement with ACT DR6 genuine or an artifact?

    Authors: We agree that the standard prescription is ε_V(τ_end)=1 and that imposing η_V(τ_*) at the observational value is the predictive way to read off n_s. In our potential the slow-roll parameter ε_V remains very small throughout the plateau (this is the source of the small r) and ε_V → 1 is reached only after a very long traverse of τ, while η_V exits the slow-roll window first; this is why we operationally defined τ_end through η_V. We acknowledge that, as written, varying η_V(τ_end) over {-0.0125,…,-0.0095} effectively tunes n_s and so the ‘consistency with ACT DR6’ in Figs. 7, 8, 13 partly reflects the choice of endpoint rather than a sharp prediction. In v3 we will: (i) redefine τ_end by ε_V(τ_end)=1 and recompute n_s, r, N_e at τ_* on that basis; (ii) report the resulting (n_s, r) as the genuine prediction, and present the η_V(τ_end) variation only as a sensitivity study with that interpretation made explicit; (iii) verify and quote ε_V(τ_end) at the points previously used, so the reader can see the size of the prescription dependence. revision: yes

  3. Referee: §4.2, Fig. 14: the claim that the predicted GW signal lies within the detectable range is not supported by the spectra shown; only CMB B-mode probes the relevant frequencies for r ≳ 10^{-3.6}.

    Authors: The referee is correct. With r_{0.002} in the range 10^{-5}–10^{-3.6} the spectra shown in Fig. 14a fall below the LISA/ET/BBO sensitivity envelopes by several orders of magnitude. The only channel with realistic sensitivity at the relevant scales is CMB B-mode polarization (LiteBIRD, CMB-S4, BICEP/Keck/SPIDER successors), which probes f ~ 10^{-18}–10^{-16} Hz. In v3 we will rewrite §4.2 to state this explicitly: direct-detection interferometers cannot reach the predicted Ω_GW h^2, while the upper end of our r range (~10^{-3.6}) is within reach of next-generation CMB B-mode experiments and the lower end is not. The metadata-abstract phrasing ‘too small to yield a detectable gravitational wave signal’ was correct for direct detection but misleading regarding CMB B-modes; we will phrase the conclusion accordingly. revision: yes

  4. Referee: §2, Eq. (2.17): the single-field reduction relies on m_ω² ≳ (3q²/2) M_P² being above the inflation scale, justified only by q ≳ 1 / WGC. Provide a quantitative bound on q and check the ACT-compatible points lie above it.

    Authors: We agree the bound should be made quantitative. The decoupling condition is m_ω² = (3q²/2) M_P² δ(τ) ≫ H_inf² ≃ V_*/(3 M_P²), i.e. q² ≫ (2/9) V_*/(M_P^4 δ). With δ ≳ 1 (Fig. 1) and V_*^{1/4} ≲ 1.6×10^{16} GeV at the Planck bound, this gives a numerical threshold q_min ≪ 1 for the points retained in Figs. 8, 12, 13; the WGC-motivated range q ~ O(1) used here sits well above it. However, the referee is right that we did not state this explicitly. In v3 we will (i) derive q_min(ξ_0,p,τ_*) explicitly, (ii) overlay it on the parameter-space figures, and (iii) verify point by point that the ACT-compatible parameter points satisfy q ≫ q_min. We will also note the regime q ≲ q_min as out of scope of the present single-field analysis, as already flagged in the Conclusions. revision: yes

  5. Referee: §4.1, Eq. (4.13): µ = H_inf is implicit and self-referential. Demonstrate uniqueness of the solution and that the µ_1 vs µ_2 insensitivity (≤5% in couplings) propagates to ≪ 1σ in n_s.

    Authors: We agree this should be made explicit. (i) Existence/uniqueness: V_{1-loop}(τ=10², H, µ=H) is a smooth, monotonically increasing function of H over the relevant range (the curvature-dependent logs grow only logarithmically while the M_P^{-2} prefactor on the right-hand side of 3 M_P² H² = V_{1-loop} dominates), so the fixed-point equation H² = V_{1-loop}/(3 M_P²) admits a unique positive root in every parameter point we scanned; we verified this numerically and will include the argument and a representative plot in an appendix in v3. (ii) Propagation to n_s: the ≤5% spread in couplings between the µ_1 and µ_2 prescriptions translates into Δn_s well below 10^{-3} (much smaller than the ACT 1σ uncertainty 0.003) and Δlog_{10} r below 0.05; we will quote these numbers explicitly in v3 and confirm that the boundary log_{10} p ≥ -log_{10} ξ_0 + 4.2 in Fig. 11 is stable under the prescription change at the level of the figure resolution. revision: yes

standing simulated objections not resolved
  • We cannot, within the present single-field framework, make a quantitative prediction in the regime q ≲ q_min where the Weyl vector ω_µ does not decouple from the inflaton; that regime requires a genuinely two-field (inflaton + ω_µ) treatment which is outside the scope of this paper and is left for future work, as already noted in the Conclusions.

Circularity Check

2 steps flagged

Derivation chain is largely self-contained against external benchmarks; the only mild concern is tuning η_V(τ_end) to recover the observed n_s, which is a fitting choice rather than a true circularity.

specific steps
  1. fitted input called prediction [Section 3, around Fig. 7; Section 4, around Fig. 13; Fig. 8]
    "The final value of the scalar spectral index n_s is primarily influenced by the choice of η_V(τ_end). Therefore, by redefining the end of inflation, τ_end, consistently with the observational constraints, it is possible to achieve results in agreement with experimental data."

    The end of inflation is normally fixed by a slow-roll breakdown criterion (e.g. |η_V|=1). Here, η_V(τ_end) is instead chosen per parameter point (≈ −0.0095 to −0.0125) so that n_s lands in the Planck/ACT band. This converts what is presented as a 'prediction' for n_s into a one-parameter fit per (ξ_0, p) point. Disclosed and not strictly tautological (r_{0.002} is still an output), so it lowers predictive content rather than fully collapsing the derivation.

  2. self citation load bearing [Section 4, item on propagator suppression factors; Appendix C]
    "Following the approach in [34–37], we account for modifications in the commutation relations that arise when transforming between frames. This introduces the propagator suppression factors c_{ϕi}, which affect the β functions obtained in the Jordan frame."

    The c_{ϕi} suppression factors that drive the modified RG running (and hence the quantum-corrected n_s, r_{0.002}) are imported from refs [34–37] (Lee; Lerner & McDonald; Salopek–Bond–Bardeen). These are external authors, not self-citations, and the construction is reproduced explicitly in Appendix C from the canonical commutator. So this is load-bearing on a citation but the citation is independent and the derivation is shown — not circular, listed only for completeness.

full rationale

The paper's logical chain is: (i) write a scale-invariant Higgs–dilaton Lagrangian in Weyl geometry, (ii) fix three parameters (λ_0, λ_1, λ_2 relations and ξ_0, ξ_1 normalization) by demanding M_P = 2.44·10^18 GeV, ⟨ϕ_1⟩ = 250 GeV, m_H = 125 GeV at the vacuum (Appendix B), (iii) compute slow-roll observables n_s, r_{0.002} on the resulting potential and compare to Planck/ACT. Steps (ii) and (iii) use independent inputs: vacuum-scale data calibrates parameters; CMB-scale observables are then computed predictions. That is standard model-building, not circularity. The one methodological soft spot is in §3 and §4: the endpoint of inflation is defined ad hoc as η_V(τ_end) = −0.0095 (rather than the standard |η_V|=1 or ε_V=1), and when the resulting n_s misses the Planck/ACT central value, the authors openly state "by redefining the end of inflation, τ_end, consistently with the observational constraints, it is possible to achieve results in agreement with experimental data" (§3, around Fig. 7) and tune η_V(τ_end) per parameter point (Fig. 8, Fig. 13). This is a fit-to-data move dressed as a model prediction, but it is disclosed; it lowers the predictive content of n_s but does not collapse the derivation into a tautology — r_{0.002} and the GW spectrum remain genuine outputs given the (ξ_0, p) choice. Self-citations (e.g., [21] Lalak & Michalak, and the Ghilencea Weyl-geometry stack [1–12]) are background framework, not load-bearing uniqueness arguments. The Weyl-geometry construction is taken from external literature; nothing here imports a "uniqueness theorem" from the authors' own prior work to forbid alternatives. The skeptic's headline concern (abstract vs §5 disagreement on whether Λ_UV sits above or below the inflationary scale) is a self-consistency / correctness contradiction between v1 and v2 framing, not a circular derivation. It belongs under correctness risk, not under this axis. Overall: score 2.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Model omitted the axiom ledger; defaulted for pipeline continuity.

pith-pipeline@v0.9.0 · 9563 in / 7784 out tokens · 117265 ms · 2026-05-06T17:46:26.989264+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.